14 lines
266 B
Text
14 lines
266 B
Text
|
Require Import Utf8.
|
||
|
|
|
||
|
|
Section FOLD.
|
||
|
|
Context {A: Type} (f: A → A) (a: A).
|
||
|
|
Fixpoint fold (n: nat) : A :=
|
||
|
|
match n with
|
||
|
|
| O => a
|
||
|
|
| S n' => f (fold n')
|
||
|
|
end.
|
||
|
|
End FOLD.
|
||
|
|
|
||
|
|
Definition ackermann : nat → nat → nat :=
|
||
|
|
fold (λ g, fold g (g (S O))) S.
|