Ackermann function: Difference between revisions

Content added Content deleted

Inline

@@ Line 2,803: / Line 2,803: @@
 =={{header|Coq}}==
+===Standard===
-<syntaxhighlight lang="coq">Require Import Arith.
+<syntaxhighlight lang="coq">
 Fixpoint A m := fix A_m n :=
   match m with
@@ Line 2,812: / Line 2,813: @@
         | S pn => A pm (A_m pn)
       end
-  end.</syntaxhighlight>
+  end.
+</syntaxhighlight>
+===Using fold===
-<syntaxhighlight lang="coq">Require Import Utf8.
+<syntaxhighlight lang="coq">
+Require Import Utf8.
 Section FOLD.
-  Context {A: Type} (f: A → A) (a: A).
+  Context {A : Type} (f : A → A) (a : A).
-  Fixpoint fold (n: nat) : A :=
+  Fixpoint fold (n : nat) : A :=
     match n with
-    | O => a
+      | O => a
-    | S n' => f (fold n')
+      | S k => f (fold k)
     end.
 End FOLD.