Coq中的段机制。禁止省略上下文中的假设
提问于 2019-02-21 10:33:54
我需要更原始的泛化机制。例如,
Section sec.
Context (n:nat).
Definition Q:=bool.
End sec.
Check Q.我将获得q: Set，但我需要Q:nat->Set。
我尝试了上下文，假设，变量。它不起作用。如何获得这样的行为？
回答 1
Stack Overflow用户
回答已采纳
发布于 2019-02-21 17:31:04
但是，这不是使用Definition ... :=可以完成的事情，您可以使用Proof using
Section sec.
Context (n:nat).
Definition Q : Set.
Proof using n.
exact bool.
Defined.
End sec.
Check Q.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/54804957
复制
腾讯云开发者
