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: May 02 2025 at 03:31 UTC