我正在研究在Coq中使用显式宇宙
构建一个固定的宇宙层次结构的可能性。尝试使用常量(2、3、4)来构建它失败了:最终,所有组合仍然可以通过类型检查(即所有声明的宇宙被视为等级上任意):
Universe k l m x y z.
Let x := 2.
Definition k := Type@{x}.
Notation y := 3.
Definition l := Type@{y}.
Notation z := 4.
Definition m := Type@{z}.
Print x. (*x = 2: nat*)
Print y. (*Notation y := 3*)
Check l:k:m.
Check m:k:l.
Check k:m:l.
请注意,
Definition k := Type@{2}
和 Definition k := Type@{x+1}
会导致语法错误。是否可以使用显式宇宙来构建一个固定的层次结构,如果可以,如何实现?