Commit 2026-11-10 12:28 30c2c73a
View on Github →fix(Data/ENat/Defs): derive Repr for ℕ∞ (#45761)
Small fix.
ENat is a def for WithTop ℕ, so WithTop.instRepr is not found and repr (5 : ℕ∞) fails to elaborate.
Fixes #45740.
fix(Data/ENat/Defs): derive Repr for ℕ∞ (#45761)
Small fix.
ENat is a def for WithTop ℕ, so WithTop.instRepr is not found and repr (5 : ℕ∞) fails to elaborate.
Fixes #45740.