Zulip Chat Archive
Stream: mathlib4
Topic: rename `Nat.le_or_eq_or_le_succ`
Bulhwi Cha (Jan 08 2023 at 12:59):
Shouldn't Nat.le_or_eq_or_le_succ be renamed Nat.le_or_eq_of_le_succ?
Bulhwi Cha (Jan 09 2023 at 04:46):
I've opened PRs: lean4#2024 and std4#81. I should've put the question on #lean4.
Last updated: Dec 20 2023 at 11:08 UTC