siddhartha-gadgil

forever : ℕ → ℕ
forever zero = zero
forever (succ n) = forever (succ (succ n))

siddhartha-gadgil

_*_ : ℕ → ℕ → ℕ
zero * n = zero
(succ m) * n = n + (m * n)


factorial : ℕ → ℕ
factorial zero = succ zero
factorial (succ n) = (succ n) * (factorial n)

siddhartha-gadgil

data List (A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A

siddhartha-gadgil

{-# BUILTIN NATURAL ℕ #-}
{-# BUILTIN ZERO zero #-}
{-# BUILTIN SUC succ #-}

siddhartha-gadgil

open import Nat

onetwothree : List ℕ
onetwothree = 1 :: (2 :: (3 :: []))

siddhartha-gadgil

length₀ : (A : Set) → List A → ℕ
length₀ _ [] = zero
length₀ A (a :: l) = succ (length₀ A l)

siddhartha-gadgil

length : {A : Set} → List A → ℕ
length [] = zero
length (a :: l) = succ (length l)

siddhartha-gadgil

_++_ : {A : Set} → List A → List A → List A
[] ++ l = l
(a :: xs) ++ l = a :: (xs ++ l)

reverse : {A : Set} → List A → List A
reverse [] = []
reverse (a :: l) = (reverse l) ++ (a :: [])

siddhartha-gadgil

_map_ : {A B : Set} → List A → (A → B) → List B
[] map _ = []
(a :: xs) map f = (f a) :: (xs map f)

twothreefour : List ℕ
twothreefour = onetwothree map succ

siddhartha-gadgil

_flatMap_ : {A B : Set} → List A → (A → List B) → List B
[] flatMap _ = []
(a :: xs) flatMap f = (f a) ++ (xs flatMap f)