![]() |
1
1
排序约束的检查可以在ML级别上暂时禁用,然后重新激活。(请参见下面的完整示例。)但该解决方案看起来非常像黑客。我们必须更改上下文中的排序约束,并记住在之后恢复它们。
这一理论被Isabelle/HOL接受。这种方法适用于更复杂的环境(我已经使用过几次),但我更喜欢更优雅的方法。 |
![]() |
2
1
下面是一个不同的解决方案,在证明引理后不需要“清理”( this answer 之后需要“修复”排序约束)。
这个想法是定义一个新常数(
这种方法的缺点是,在证明引理的过程中,我们永远不能明确地写出任何包含
|