Zulip Chat Archive

Stream: mathlib4

Topic: simp? drops ←

Johan Commelin (Jan 05 2023 at 14:23):

Consider https://github.com/leanprover-community/mathlib4/pull/966/files#diff-54ef6c59abdddf67950b1ee785a0c22c7e03d04f9ad8cdb7cf1d336a72f4d850R1882

If you change simp to simp? then the output will drop the ← in front of the lemma that should be applied right-to-left.

Last updated: Dec 20 2025 at 21:32 UTC