勒柯克：居住在组非列表的数据结构？(Coq: Non-list Data structures li

如果我有以下线：

Definition Foo : Set := list nat.

然后我编译没有问题。

然而，假设我想要做同样的Coq.Lists.ListSet ，较有限集为列表库：

(*Section first_definitions.
 Variable A : Type.
Definition listset := list A.*)
Definition Bar : Set := listset nat.

我得到以下错误：

The term "listset nat" has type "Type" while it is expected to have type 
"Set" (universe inconsistency).

1. 有没有一种方法，以“铸造” listset ，使其生活在Set而不是Type ？ 即如果我知道我将要使用listset参数类型Set ，有没有办法让它活在Set层次结构不知何故？
2. 为什么会发生的错误listset ，而不是list ，当listset被定义为list ？

注 ：实际类型称为set ，但我已经重新命名为listset以避免与排序混乱Set 。

编辑： =取代:=

Answer 1:

2. 为什么发生了LISTSET的错误，而不是列表中，当LISTSET被定义为列表？

由于list是一个模板宇宙多态性归纳定义（见About list. ），在这种情况下意味着，如果list中用于一类Set ，结果仍是Set 。

1. 有没有一种方法，以“铸造” listset ，使其生活在Set而不是Type ？

据我所知，有没有办法让定义模板的宇宙多态的，但你可以让他们的宇宙多态 ，像这样：

Polymorphic Definition listset (A : Type) : Type := list A.
Check listset nat : Set.

还有一个选择是使用Set Universe Polymorphism命令，这样你就不需要用预先考虑您的定义Polymorphic的关键字。 此功能在有写作的时候实验状态。 它不具有追溯力，所以我想你会需要到餐桌自己ListSet 。

文章来源: Coq: Non-list Data structures living in Set?