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

我有一个类型签名(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)

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

（编辑：安卓应用网）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!