我从“残酷的 Agda 简介” http://oxij.org/note/BrutalDepTypes/
假设我们想在偶数上定义除以二。我们可以这样做：
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
当你评估表达式 div (succ (succ zero)) 你得到 \p -> succ zero 这就是你所期望的。但是，我不明白的是如何解释 \p. 我也不明白代码 f : \bot -> N f = div (succ zero) 是什么意思。我知道 \bot 对任何 A 都意味着 A ...因此类型是有效的。我想我认为依赖类型将允许我以这样的方式编写 div，即 div (succ zero) 会更明确地失败类型检查。
任何人都可以就如何在 agda 中使用和查看谓词提出建议吗？