search

leanprover-community / mathlib4

The math library of Lean 4
https://leanprover-community.github.io/mathlib4_docs
Apache License 2.0
1.39k stars 310 forks source link

tracking issue for change in behaviour in `@[simp] def` #11647

Open kim-em opened 6 months ago

kim-em commented 6 months ago

Back in Lean 3, @[simp] def f only unfolded suitably applied appearances of f. In Lean 4, it means it can be unfolded unapplied.

This resulted in many @[simp] attributes being removed from definitions, and replaced by explicit @[simp] lemmas.

This issue is a tracking issue for places where adaptations were required for this that may warrant further investigation. Often during the port this was worked around using @[eqns], but with changes to the generation of equation lemmas this approach has become less reliable.

kim-em commented 6 months ago

Please feel free to edit the description to provide better/more detailed explanation of the change.

kim-em commented 6 months ago

Some instances of #11119 should perhaps be updated to point here.