mathlib
839b92fe - feat(data/nat/enat): new file (#16217)

Commit
3 years ago
feat(data/nat/enat): new file (#16217) Define `enat := with_top nat`, use notation.
Author
Parents
Loading