Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-09 04:34 6dd9a54c

View on Github →

feat(tactic/simps): allow composite projections (#7074)

  • Allows custom simps-projections that are compositions of multiple projections. This is useful when extending structures without the old_structure_cmd.
  • Coercions that are compositions of multiple projections are not automatically recognized, and should be declared manually (coercions that are definitionally equal to a single projection are still automatically recognized).
  • Custom simps projections should now be declared using the name used by simps. E.g. equiv.simps.symm_apply instead of equiv.simps.inv_fun.
  • You can disable a projection proj being generated by default by simps using initialize_simps_projections (-proj)

Estimated changes