Coq：生活在 Set 中的非列表数据结构？
Coq: Non-list Data structures living in Set?
如果我有以下行：
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).
- 有没有办法 "cast"
listset 使其位于 Set 而不是 Type？也就是说，如果我知道我将使用 listset 和 Set 类型的参数，有没有办法让它以某种方式存在于 Set 等级制度中？
- 当
listset 定义为 list 时，为什么 listset 会出现错误，而 list 不会出现错误？
注意：实际的类型叫做set，但是我把它重命名为listset以避免和排序[=15=混淆].
编辑：= 替换为 :=
- Why does the error happen for listset, but not for list, when listset is defined to be list?
因为list是一个template universe polymorphic归纳定义（参见About list.），在这种情况下意味着如果list应用于[=14]中的类型=]，结果还在Set.
- Is there a way to "cast"
listset so that it lives in Set instead of Type?
AFAIK，没有办法让定义模板 universe 多态，但你可以让它们 universe polymorphic 像这样：
Polymorphic Definition listset (A : Type) : Type := list A.
Check listset nat : Set.
另一种选择是使用 Set Universe Polymorphism 命令，这样您就不需要在定义前加上 Polymorphic 关键字。
此功能在撰写本文时处于实验状态。而且它不追溯适用，所以我想你需要自己分叉 ListSet.
如果我有以下行：
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).
- 有没有办法 "cast"
listset使其位于Set而不是Type？也就是说，如果我知道我将使用listset和Set类型的参数，有没有办法让它以某种方式存在于Set等级制度中？ - 当
listset定义为list时，为什么listset会出现错误，而list不会出现错误？
注意：实际的类型叫做set，但是我把它重命名为listset以避免和排序[=15=混淆].
编辑：= 替换为 :=
- Why does the error happen for listset, but not for list, when listset is defined to be list?
因为list是一个template universe polymorphic归纳定义（参见About list.），在这种情况下意味着如果list应用于[=14]中的类型=]，结果还在Set.
- Is there a way to "cast"
listsetso that it lives inSetinstead ofType?
AFAIK，没有办法让定义模板 universe 多态，但你可以让它们 universe polymorphic 像这样：
Polymorphic Definition listset (A : Type) : Type := list A.
Check listset nat : Set.
另一种选择是使用 Set Universe Polymorphism 命令，这样您就不需要在定义前加上 Polymorphic 关键字。
此功能在撰写本文时处于实验状态。而且它不追溯适用，所以我想你需要自己分叉 ListSet.