Commit 2021-04-09 04:34 6dd9a54c

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)