Def Nat.Upto

Modification history

2024-05-07 01:05
Mathlib/Data/Nat/Upto.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted Nat.UptoView on Github →
2022-12-14 15:48
Mathlib/Data/Nat/Upto.lean
feat port: Data.Nat.Upto (#1020) …
Added Nat.UptoView on Github →