idris – 在条件语句分支中指定条件为真的依赖函数

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)

这不是我们可以轻易地做的只是布尔值.