remove Nat-specific equality
This commit is contained in:
parent
0994ae2940
commit
12af0730eb
@ -119,13 +119,6 @@ fromInteger n
|
||||
| n T.> 0 = S (fromInteger (T.pred n))
|
||||
|
||||
|
||||
-- | Equality for natural numbers
|
||||
(≡) ∷ ℕ → ℕ → 𝔹
|
||||
Z ≡ Z = T
|
||||
(S n) ≡ (S m) = n ≡ m
|
||||
_ ≡ _ = F
|
||||
|
||||
|
||||
-- | Infinity
|
||||
(∞) ∷ ℕ
|
||||
(∞) = S (∞)
|
||||
|
Loading…
Reference in New Issue
Block a user