为什么这会通过Liquid Haskell验证?
{-@ sub :: Nat -> Nat -> Int @-}
sub :: Int -> Int -> Int
sub i j = i - j
从LH的角度来看,这是否意味着Nat
相同Int
?
假设您对我说:“嘿,我想要一个苹果!”。我回答:“对不起,我只有红苹果。” 你会很有趣地看着我,对吧?红苹果就是苹果!
如果一个函数要求一个Int
as作为参数,则将它传递给Int
您知道不是负数的an没问题。
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句