Macro for spread syntax (__ := instSomething
) in structures. #
Mathlib extension to preserve old behavior of structure instances.
We need to be able to let
some implementation details that are still local instances.
Normally implementation detail fvars are not local instances,
but we need them to be implementation details so that simp
will see them as "reducible" fvars.
Equations
Instances For
Mathlib extension to preserve old behavior of structure instances.
We need to be able to let
some implementation details that are still local instances.
Normally implementation detail fvars are not local instances,
but we need them to be implementation details so that simp
will see them as "reducible" fvars.