September 2017 Update
This commit is contained in:
parent
bba7bfd280
commit
ba8067c3b7
14570 changed files with 153136 additions and 63871 deletions
12
Task/Ackermann-function/Agda/ackermann-function-1.agda
Normal file
12
Task/Ackermann-function/Agda/ackermann-function-1.agda
Normal file
|
|
@ -0,0 +1,12 @@
|
|||
open import Data.Nat
|
||||
open import Data.Nat.Show
|
||||
open import IO
|
||||
|
||||
module Ackermann where
|
||||
|
||||
ack : ℕ -> ℕ -> ℕ
|
||||
ack zero n = n + 1
|
||||
ack (suc m) zero = ack m 1
|
||||
ack (suc m) (suc n) = ack m (ack (suc m) n)
|
||||
|
||||
main = run (putStrLn (show (ack 3 9)))
|
||||
2
Task/Ackermann-function/Agda/ackermann-function-2.agda
Normal file
2
Task/Ackermann-function/Agda/ackermann-function-2.agda
Normal file
|
|
@ -0,0 +1,2 @@
|
|||
agda --compile Ackermann.agda
|
||||
./Ackermann
|
||||
Loading…
Add table
Add a link
Reference in a new issue