我最近问过这个问题: 该类型中使用的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 …