如何解决重新排序假设在Coq中的显示?
是否有一种策略可以在Coq证明内重新排列假设的显示顺序。在使用归纳法时(假设很长),很多时候,我想将所有定义和所有其他方程式一起打印出来。
解决方法
只需澄清一下,Coq确实带有重新排列假设的策略。 这些是listed in the documentation
即您将对此感兴趣
move h before h'.
move h after h'.
move h at top.
move h at bottom.
文档附带有用的示例,但名称应不言自明。
,Coq没有附带任何东西,但是Pierre Courtieu的LibHyps为此提供了一些便利。特别是:
Require Import LibHyps.LibHyps.
onAllHyps move_up_types.
应该执行您想要的。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。