Zulip Chat Archive
Stream: mathlib4
Topic: non-terminal `simp`s
Yury G. Kudryashov (Jul 15 2023 at 18:15):
Can we have a linter (or an option) that bans non-terminal simps without only?
Yury G. Kudryashov (Jul 15 2023 at 18:15):
Some of them appeared during the port.
Last updated: May 02 2025 at 03:31 UTC