时间戳

首页 > 解决方案 > 如何在 Coq 的类属性中使用表示为列表的有限集？

coq - 如何在 Coq 的类属性中使用表示为列表的有限集？

问题描述

我正在使用 Coq 标准库中的 ListSet 扩展，以使用有限集作为类的属性： 

Require Import ListSet.
Class aux := {
  attribute1: set;
  attribute2: set -> set;
  }.

但我收到此错误：

Error: In environment
aux : Type
The term "set" has type "Type -> Type" which should be Set, Prop or Type.

我不明白为什么会这样。（我是 Coq 的新手）

标签： coq

解决方案

Coq 告诉你这set不是类型，而是类型，Type -> Type意思是它需要一个类型作为参数。

如果您查看定义：https ://coq.inria.fr/library/Coq.Lists.ListSet.html 您可以看到它确实需要一个参数。因此，您要考虑的类型是set A某种类型A，实际上它只是 type list A，ListSet模块带来的是set A保留不变量的操作，例如您没有两次相同的元素。

也许这些不是你想到的集合。

推荐阅读