我最近问了这个问题： 类型中使用的 agda 命题——这是什么意思？ 并收到了关于如何使类型隐式并获得真正的编译时错误的深思熟虑的答案。
但是，我仍然不清楚如何创建具有依赖类型的值。
考虑：
div : (n : N) -> even n -> N
div zero p = zero
div (succ (succ n)) p= succ (div n p)
div (succ zero) ()
其中N是自然数，偶数是下面的命题。
even : N -> Set
even zero = \top
even (succ zero) = \bot
even (succ (succ n)) = even n
data \bot : Set where
record \top : Set where
假设我想写一个函数如下：
f : N -> N
f n = if even n then div n else div (succ n)
我不知道如何以我想要的方式做这样的事情......在我看来，最好的办法是证明（不是（甚至 n））\甚至（成功 n）。我真的不知道如何在 agda 中表达这一点。我能写
g : (n:N) -> (even n) -> (even (succ n)) -> N
g n p q = if evenB n then (div n p) else (div (succ n) q)
由此，我可以做如下事情：
g 5 _ _
并评估为正常形式......以获得答案。如果我想写 f，我可以这样做
f n = g n ? ?
我得到 fn = gn { }1 { }2 其中 ?1 = 偶数 n，而 ?2 = 偶数 (succ n)。然后我可以做 f 5 之类的事情并评估为正常形式。我真的不明白为什么这是有效的......有没有办法告诉agda更多关于f以这种方式定义的信息。我可以确定如果 ?1 失败 ?2 会成功，那么告诉 agda 评估 f 总是有意义的吗？
我将 g 解释为一个函数，它接受一个数字 n，一个 n 是偶数的证明，一个 (succ n) 是偶数的证明，并返回一个数字。（这是阅读本文的正确方法吗？或者有人可以提出更好的阅读方法吗？）我真的很想准确（或更准确地）理解上述类型的检查方式。它是否使用感应 - 它是否将 (evenB n) 与 p 连接：甚至 n？等等。我现在很困惑，因为它知道
if evenB n then (div n q) else (whatever)
if evenB n then div (succ n) q else div n p
不正确。首先我明白为什么 - q 代表 succ n，所以它不匹配。但是第二次失败了，而且原因更加神秘，而且似乎阿格达比我想象的还要强大……
如果我能弄清楚该怎么做（如果有意义的话），这是我非常喜欢的第一步。
g : (n : N) -> (even n) -> N
g n p = if evenB n then (div n p) else (div (succ n) (odd p))
其中奇数 p 证明如果偶数 n 是荒谬的，那么 succ n 是偶数。我想，这将要求我能够使用依赖类型的值。
最终，我希望能够写出这样的东西：
g : N -> N
g n =
let p = proofthat n is even
in
if evenB n then div n p else (div (succ n) (odd p))
或类似的规定。甚至
g : N -> N
g n = if evenB n then let p = proofThatEven n in div n p else let q = proofThatEven succ n in div n q
我真的很想知道如何制作与依赖类型相对应的证明，以便我可以在程序中使用它。有什么建议么？