return to top
source
Extended natural numbers ℕ∞ = WithTop ℕ.
ℕ∞ = WithTop ℕ
Recursor for ENat using the preferred forms ⊤ and ↑a.
ENat
⊤
↑a