Trying out agda

demo.agda

module demo where

-- Natural numbers

data ℕ : Set where
    zero : ℕ
    suc  : ℕ → ℕ
{-# BUILTIN NATURAL ℕ #-}

infix 5 _+_
_+_ : ℕ → ℕ → ℕ
n + zero = n
n + (suc m) = suc (n + m)

infix 10 _*_
_*_ : ℕ → ℕ → ℕ
n * zero = zero
n * (suc m) = n * m + n



-- Lists

data List (A : Set) : Set where
    nil  : List A
    cons : (x : A) → (xs : List A) → (List A)

infixr 100 _,_
_,_ : {A : Set} → A → (List A) → (List A)
x , y = cons x y

len : {A : Set} -> (List A) → ℕ
len nil = zero
len (cons _ xs) = suc (len xs)

infixr 1000 _++_
_++_ : {A : Set} → (List A) → (List A) → (List A)
nil ++ ys = ys
(cons x xs) ++ ys = cons x (xs ++ ys)

reverse : {A : Set} → (List A) → (List A)
reverse nil = nil
reverse (cons x xs) = (reverse xs) ++ (x , nil)