diff --git a/examples/nat.quox b/examples/nat.quox index 36ce76c..37acff0 100644 --- a/examples/nat.quox +++ b/examples/nat.quox @@ -83,7 +83,7 @@ def eq? : DecEq ℕ = } }; -def eqb : 1.ℕ → 1.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n); +def eqb : ω.ℕ → ω.ℕ → Bool = λ m n ⇒ dec.bool (m ≡ n : ℕ) (eq? m n); def0 plus-zero : 0.(m : ℕ) → m ≡ plus m 0 : ℕ =