问Coq:释放宇宙
EN

Stack Overflow用户

提问于 2017-03-19 04:04:25

回答 1查看 97关注 0票数 0

有没有办法在Coq中Reset (或者更广泛地说，是免费的)领域？

Universe M.
Print Sorted Universes. (*M = Type.2*)
Fail Print M. (*Error: M not a defined object.*)
Reset M.
Print Sorted Universes. (*M = Type.2*)
Definition M := Type@{M}.
Print M. (*M = Type: Type*)
Print Sorted Universes. (*M = Type.2*)
Reset M.
Fail Print M. (*Error: M not a defined object.*)
Print Sorted Universes. (*M = Type.2*)

不管我做什么，M = Type.2。我在Coq 8.5

coq

回答 1

Stack Overflow用户

发布于 2017-04-09 03:35:06

我找到了两种方法。Reset Initial会破坏整个环境(这通常不只是一个人想要的)。另一种方法是使用模块来掩蔽宇宙

Universe M R. Constraint M < R.
Definition M := Type@{M}. Definition R := Type@{R}.
Check M:R. Fail Check R:M. (*the hierarchy holds*)

(*1. w/ modules:*)
Module i.
Universe M R. Constraint R < M.
Check M:R. Fail Check R:M. (*still holds*)
Definition M := Type@{M}. Definition R := Type@{R}. (*but now..*)
Fail Check M:R. Check R:M.  (*not any more*)
Print Sorted Universes. (*2 Rs and Ms, w/ the old hierarchy masked by the new one*)
End i.

(*outside the module the old hierarchy holds*)
Check M:R. Fail Check R:M.

(*2. w/ Reset Initial:*)
Reset Initial. Fail Check M:R. Fail Check R:M.
Print Sorted Universes. (*the def-d univ-s are gone*)

票数 0

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/42879246

复制

相似问题

问Coq:释放宇宙
EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Coq:释放宇宙EN

回答 1

Stack Overflow用户

社区

活动

圈层

关于

腾讯云开发者

热门产品

热门推荐

更多推荐

问Coq:释放宇宙
EN