我发现 Isabelle/HOL 中的许多定理更喜欢元级蕴涵：
==>
代替
-->
对象逻辑级别，即高阶逻辑含义。
伊莎贝尔维基说粗略地说，应该使用元级别含义将规则语句中的假设与结论分开.
除此之外，关于对象和元级别含义的使用我应该了解什么？我发现后者被大多数使用。我应该何时以及为何使用 HOL 蕴涵？
我认为简短的答案是：使用==>只要有可能，因为它比合作更容易-->.
话虽这么说，你不应该看到==>在您编写的代码中经常出现。
- 编写引理时，使用
assumes and shows syntax.
- 对于中间步骤
have有一个语法if:
have "B" if "A"代替have "B ==> A"
- 元蕴含只能在顶层使用，因此如果您有一个谓词作为函数的参数，则不能使用
==>在那个谓词中。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
