module Demo where

-- Read Set as kind *; 
data Bool : Set where
  true : Bool -- look no capitals!
  false : Bool

-- Ctrl-c Ctrl-l -- loads the file and type checks
-- Ctrl-c Ctrl-c -- pattern match on a variable in the hole
-- Ctrl-c Ctrl-space -- complete the hole with the current text
-- Ctrl-c Ctrl-f -- go forward to the next hole
-- Ctrl-c Ctrl-, -- tell me what is in scope in this hole
data ℕ : Set where
  zero : ℕ
  succ : ℕ → ℕ -- write \to instead of ->

not : Bool → Bool
not true = false
not false = true

_∧_ : Bool → Bool → Bool
false ∧ b = false
true ∧ b = b

_∨_ : Bool → Bool → Bool
true ∨ b = true
false ∨ b = b

cond : forall (a : Set) → Bool → a → a → a
cond a true t e = t
cond a false t e = e

id : forall {a : Set} → a → a
id x = x

id-bool : Bool → Bool
id-bool = id {Bool}

cond-example : ℕ
cond-example = cond _ (true ∧ false) zero (succ zero)

id-example : ℕ
id-example = id zero

-- Ctrl-c Ctrl-n -- normalise an expression