为什么在Liquid Haskell中Nat类型等于Int?

随机B

为什么这会通过Liquid Haskell验证?

{-@ sub :: Nat -> Nat -> Int @-}                                                                                                         
sub :: Int -> Int -> Int 
sub i j = i - j 

从LH的角度来看,这是否意味着Nat相同Int

丹尼尔·瓦格纳

假设您对我说:“嘿,我想要一个苹果!”。我回答:“对不起,我只有苹果。” 你会很有趣地看着我,对吧?红苹果就是苹果!

如果一个函数要求一个Intas作为参数,则将它传递给Int您知道不是负数的an没问题

本文收集自互联网,转载请注明来源。

如有侵权,请联系 [email protected] 删除。

编辑于
0

我来说两句

0 条评论
登录 后参与评论

相关文章

Liquid Haskell中的“ map”函数的正确约定是什么?

为什么在zsh中“ \\\\”等于“ \\”?

为什么(列表类型)等于CONS?

为什么 Agda 中的 Haskell 类型类以“Raw”开头?

为什么Haskell中没有`Cofunctor`类型类?

为什么输入参数等于对象类型等于?

为什么unsigned int在haskell中如此罕见?

为什么{} == {}等于false?

为什么 !&&等于||?

为什么+ !! {}等于1?

为什么01001000等于Binary中的H

为什么Coq中的所有数字文字都显示nat类型?

为什么Idris中的Nat数据类型以0而不是1开头?

为什么在Java中不使用int基本类型

为什么此e / lval的类型在CIL中为int?

为什么是 int 类型错误?类型错误

为什么是SomeClass <?超级T>不等于Java泛型类型中的SomeClass <T>吗?

为什么在C中强制转换为int不等于所有双打

Haskell中<-的类型是什么?

为什么在值构造函数中声明的类型不是在Haskell中声明的类型?

为什么在Kotlin中Int是Comparable <Int>的子类型,但是HashMap不是Comparable <HashMap>的子类型

Haskell中具有类型的冒险:GADT:为什么进行以下类型检查?

为什么Haskell的作用域类型变量不允许在模式绑定中绑定类型变量?

为什么我的函数的返回类型是 a -> Int

为什么Jekyll Liquid不在哪里过滤?

为什么Jekyll的Liquid“包含”返回字符串?

为什么是char类型?

为什么1:[[]]等于(1:[]):[]?

为什么“ a” <“ b”等于“ true”?