Yuu*_*uri 5 formal-verification primitive-types idris
对于学习依赖类型,我正在重写伊德里斯的旧Haskell游戏.目前游戏"引擎"使用内置整数类型,例如Word8.我想证明一些涉及这些数字的数值属性的引理(例如,双重否定是同一性).但是,不可能对原始算术运算的行为说些什么.会是什么更好的,只使用believe_me或其他handwaving(至少在最基本的属性),或者重写使用我的代码Nat,Fin和其他"高层"数值类型？
我建议使用postulate您需要的任何原始属性，当然，只小心使用对于所讨论的数字类型实际上正确的东西（这基本上意味着要小心溢出）。所以你可以这样说：
postulate add_commutes : (x, y : Int) -> x + y = y + x
believe_me最好避免，除非您需要证明的某些计算行为。但是，说实话，在推理原语时我们仍在尝试解决这个问题......