mathlib
201d2c61 - refactor(data/nat/enat): rename `enat` to `part_enat` (#15235)

Commit
3 years ago
refactor(data/nat/enat): rename `enat` to `part_enat` (#15235) * find+replace `enat` with `part_enat`; * reflow long lines * add a sentence to the module docstring of `data.nat.enat`. I'm going to define `enat := with_top nat` and use it as the default implementation of "nat with top".
Author
Parents
Loading