module Overloading where data ℕ : Set where zero : ℕ succ : ℕ -> ℕ data Bool : Set where false : Bool -- the bit "0" true : Bool -- the bit "1" -- Addition of natural numbers addℕ : ℕ -> ℕ -> ℕ addℕ zero m = m addℕ (succ n) m = succ (addℕ n m) -- Addition of Bool ≅ ℤ/(2). addBool : Bool -> Bool -> Bool addBool false false = false addBool false true = true addBool true false = true addBool true true = false