重新排序假设在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.

应该执行您想要的。