我有一个类型签名(x,y：SomeType)的功能 – > (cond x y)= True – > SOMETYPE.当我检查if-then-else / case / with语句中的条件时,如何传递给相应分支中的函数,该条件是真的？
您可以使用DecEq来做到这一点：
add : (x,y : Nat) -> x + y < 10 = True -> Nat
add x y _ = x + y
main : IO ()
main =
let x = S Z
in let y = Z
in case decEq (x + y < 10) True of
Yes prf => print (add x y prf)
No _ => putStrLn "x + y is not less than 10"
但你不应该.
使用布尔(通过=或So)可以告诉你一些事情是真的,但不是为什么.如果你想组合证明或将它们分开来,为什么非常重要.想象一下,如果add称为需要x y < 20 - 我们不能仅仅通过我们的证据,即x y < 10 =真的,因为伊德里斯对这个操作一无所知,就是这样. 相反,您应该使用包含为什么它是真实的数据类型写上述. LTE是一种类型,不到比较：
add : (x,y : Nat) -> LTE (x + y) 10 -> Nat
add x y _ = x + y
main : IO ()
main =
let x = S Z
in let y = Z
in case isLTE (x + y) 10 of
Yes prf => print (add x y prf)
No _ => putStrLn "x + y is not less than 10"
现在,如果添加称为需要LTE(x y)20的函数,我们可以编写一个扩大约束的函数：
widen : a `LTE` b -> (c : Nat) -> a `LTE` (b + c) widen LTEZero c = LTEZero widen (LTESucc x) c = LTESucc (widen x c)
这不是我们可以轻易地做的只是布尔值.
