Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-04 23:56 12921e9e

View on Github →

feat(tactic/simps): some improvements (#5541)

  • @[simps] would previously fail if the definition is not a constructor application (with the suggestion to add option {rhs_md := semireducible} and maybe simp_rhs := tt). Now it automatically adds {rhs_md := semireducible, simp_rhs := tt} whenever it reaches this situation.
  • Remove all (now) unnecessary occurrences of {rhs_md := semireducible} from the library. There are still a couple left where the simp_rhs := tt is undesirable.
  • @[simps {simp_rhs := tt}] now also applies dsimp, simp to the right-hand side of the lemmas it generates.
  • Add some @[simps] in category_theory/limits/cones.lean
  • @[simps] would not recursively apply projections of prod or pprod. This is now customizable with the not_recursive option.
  • Add an option trace.simps.debug with some debugging information.

Estimated changes

deleted def foo.bar2
modified def foo.rfl2
added structure my_type
added def my_type_def
deleted def specify.specify5