Agdaはじめます

Combinators.agda

module Combinators where
b : {A B C : Set} -> (B -> C) -> (A -> B) -> A -> C
b x y z = x (y z)

c : {A B C : Set} -> (A -> B -> C) -> B -> A -> C
c x y z = x z y

k : {A B : Set} -> A -> B -> A
k x y = x

w : {A B : Set} -> (A -> A -> B) -> A -> B
w x y = x y y

fib.agda

{- definition of ℕ and fib -}
data ℕ : Set where
  O : ℕ
  S : ℕ → ℕ

pred : ℕ → ℕ
pred O     = O
pred (S n) = n

_+_ : ℕ → ℕ → ℕ
O     + n = n
(S n) + m = S (n + m)

_*_ : ℕ → ℕ → ℕ
O     * n = O
(S n) * m = m + (n * m)

_^_ : ℕ → ℕ → ℕ
n ^ O     = S O
n ^ (S m) = n * (n ^ m)

fib : ℕ → ℕ
fib O         = O
fib (S O)     = S O
fib (S (S n)) = (fib (S n)) + (fib n)