问题描述
现在我知道了，可以通过依赖类型来表达量词。所以我为此写了一个简单的实现“for all (a,b: N): exists (c: N): c = a + b”：
f : (a : Nat) -> (b : Nat) -> (c : Nat ** c = a + b)
f a b = (a + b ** Refl)
它有效。
现在我想知道，我可以表达这个“for all (a,b: N): exists (c: N): c > a and c
解决方法
对于 subdir3 比较，您可以使用 Data.Nat's Nat（大于）、GT（大于等于）、GTE（小于）、 LT（小于）。所以 LTE 和 GT c a 代表 LT c b 和 c > a。
对于 c < b，您可以将两个证明放入一个元组：and。例如，如果您希望 (GT c a,LT c b) 它们，则可以使用 or。
因此：
Either (GT c a) (LT c b)（但是，这个确切的示例不起作用，因为您无法定义 import Data.Nat
f : (a,b : Nat) -> (c : Nat ** (GT c a,LT c b))
，因为没有 f 所以 c。）