Documentation

Mathlib.Tactic.Spread

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.

      Equations
        Instances For