Ackermann function: Difference between revisions
→{{header|Coq}}: Updated Coq examples
(→{{header|Coq}}: Updated Coq examples) |
|||
Line 2,803:
=={{header|Coq}}==
===Standard===
<syntaxhighlight lang="coq">
Fixpoint A m := fix A_m n :=
match m with
Line 2,812 ⟶ 2,813:
| S pn => A pm (A_m pn)
end
end.
</syntaxhighlight>
===Using fold===
<syntaxhighlight lang="coq">
Require Import Utf8.
Section FOLD.
Context {A : Type} (f : A → A) (a : A).
Fixpoint fold (n : nat) : A :=
match n with
| O => a
| S
end.
End FOLD.
| |||