Zulip Chat Archive
Stream: mathlib4
Topic: order.filter.at_top_bot
Yury G. Kudryashov (Jan 24 2023 at 02:00):
I get some strange lint errors in mathlib4#1795. simpNF says that some simp lemmas don't simplify their LHS.
Yury G. Kudryashov (Jan 24 2023 at 02:00):
https://github.com/leanprover-community/mathlib4/actions/runs/3992251420/jobs/6847931395
Yury G. Kudryashov (Jan 24 2023 at 02:00):
I failed to understand what's wrong with these lemmas.
Last updated: May 02 2025 at 03:31 UTC