Macro for spread syntax (__ := instSomething) in structures.

def letImplDetailStx : Lean.ParserDescr

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

• One or more equations did not get rendered due to their size.

def elabLetImplDetail : Lean.Elab.Term.TermElab

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

• One or more equations did not get rendered due to their size.