Commit 2021-05-26 08:25 00394b75

feat(tactic/simps): implement prefix names (#7596)

• You can now write initialize_simps_projections equiv (to_fun → coe as_prefix) to add the projection name as a prefix to the simp lemmas: if you then write @[simps coe] def foo ... you get a lemma named coe_foo.
• Remove the short_name option from simps_cfg. This was unused and not that useful.
• Refactor some tuples used in the functions into structures.
• Implements one item of #5489.