siddhartha-gadgil

open import Nat

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

siddhartha-gadgil

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

siddhartha-gadgil

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

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

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

siddhartha-gadgil

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

siddhartha-gadgil

data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ

siddhartha-gadgil

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

siddhartha-gadgil

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

siddhartha-gadgil

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