5 lines
88 B
Text
5 lines
88 B
Text
|
A : Nat -> Nat -> Nat
|
||
|
|
A Z n = S n
|
||
|
|
A (S m) Z = A m (S Z)
|
||
|
|
A (S m) (S n) = A m (A (S m) n)
|