Natural numbers with infinity #
The natural numbers and an extra
⊤. This implementation uses
Part ℕ as an
ℕ∞ instead unless you care about computability.
Main definitions #
The following instances are defined:
Implementation details #
≤ are defined on
PartENat, but there is an issue with
* because it's not
0 * ⊤ should be.
mul is hence left undefined. Similarly
⊤ - ⊤ is ambiguous
so there is no
- defined on
open Classical line, various proofs are made with decidability assumptions.
This can cause issues -- see for example the non-simp lemma
toWithTopZero proved by
@[simp] lemma toWithTopZero' whose proof uses