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: Dec 20 2023 at 11:08 UTC