aparler/RosettaCodeData
1
0
Fork 0
Code Issues 12 Pull requests 3 Projects Releases Packages Wiki Activity Actions

2016 Update

Browse source
This commit is contained in:
Tina Müller 2016-12-05 22:15:40 +01:00
parent 948b86eafa
commit dcf5d15da3
7965 changed files with 139854 additions and 31002 deletions
Download patch file Download diff file Expand all files Collapse all files

0
Task/Ackermann-function/Coq/ackermann-function.coq → Task/Ackermann-function/Coq/ackermann-function-1.coq
View file

13
Task/Ackermann-function/Coq/ackermann-function-2.coq Normal file
View file

@ -0,0 +1,13 @@
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.