siddhartha-gadgil

data Bool : Set where
  true   : Bool
  false  : Bool
  

siddhartha-gadgil

not : Bool -> Bool
not true = false
not false = true

siddhartha-gadgil

_&_ : Bool → Bool → Bool
true & true = true
false & _ = false
true & false = false

siddhartha-gadgil

notnot : Bool -> Bool
notnot x = not (not x)

siddhartha-gadgil

verytrue : Bool → Bool
verytrue = λ x → x & x

siddhartha-gadgil

_xor_ : Bool → Bool → Bool
_xor_ = λ x y → (x & (not y)) || ((not x) & y)

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 ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

siddhartha-gadgil

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

siddhartha-gadgil

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