module demo where data Nat : Set where zero : Nat suc : Nat → Nat Addition _+_ : Nat → Nat → Nat zero + n = n suc m + n = suc (m + n)