![]() |
1
0
我在这里取得了一些进展:a
如果我们想使用
我相信在一个子区域内完成所有这些工作也是可能的,而且可能更可取,但我还没有完全弄清楚它的语法。 |
![]() |
2
0
虽然locale是在演算本身中实现的,因此它们的谓词可以用于任何常规命题,但通常不建议这样做。相反,您应该使用例如解释来实例化区域设置,如下例所示。
这种模式是否真的适合你的需要取决于你的应用;如果您只想拥有一个谓词,最好直接定义它,而不使用locale。 注:真正需要的是纯粹的平等;更喜欢HOL equality=,或其语法变体·。 |