为了学习依赖类型，我正在 Idris 中重写我的旧 Haskell 游戏。目前游戏“引擎”使用内置整数类型，例如Word8。我想证明一些涉及这些数字的数值属性的引理（例如，双重否定是身份）。但是，不可能对原始算术运算的行为说些什么。什么会更好，只使用believe_me 或其他手动操作（至少对于最基本的属性），或者使用Nat、Fin 和其他“高级”数字类型重写我的代码？
【问题讨论】：
标签： primitive-types idris formal-verification
我建议将postulate 用于您需要的任何原始属性，当然，请注意仅使用对所讨论的数字类型实际正确的东西（这基本上只是意味着要小心溢出）。所以你可以这样说：
postulate add_commutes : (x, y : Int) -> x + y = y + x
believe_me 最好避免使用，除非您需要一些证明的计算行为。但是，老实说，在推理原语时，我们仍在努力解决这些问题......
【讨论】：
我认为目前通常最好尽可能使用Nat。 Idris 开发人员最终计划实现一种通用机制，用于在编译中用快速原始类型替换证明友好的类型，但目前这只发生在 Nat 上。如果你真的想要，你可以通过believe_me，但你最终会得到在证明中不太容易使用的函数。请注意，如果您决定使用believe_me，那么您还应该考虑really_believe_me，这显然使类型检查器更可信。
【讨论】：