coq Qed向接收的引理提出警告
在COQ开发大型系统时，我通常会承认许多引理，并查看重要的定理是否有效，然后一一解决引理。
COQ接受QED。即使使用了允许的引理，因此有时我不能100％确定我是否解决了所有录取并需要寻求文本搜索的帮助>接纳，是否有更严格的Qed。不允许使用允许的引理证明定理？
Print Assumptions lemma_names.
似乎是一种可行的检查方法，还有其他解决方案吗？
When developing a big system in Coq, I usually admit many lemmas and see whether the important theorem works or not, and then solve lemmas one by one.
Coq accepts Qed. even with admitted lemmas, so sometimes I'm not 100% sure whether I solve all the admits and need to seek help with text search admit and Admitted, is there a more strict version of Qed. which doesn't allow theorems to be proved with admitted lemmas?
Print Assumptions lemma_names.
seems a feasible way to check, are there other solutions?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论