def Lean.Elab.Command.expandMixfix : Lean.Macro

Equations

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

def Lean.Elab.Command.expandMixfix.withAttrKindGlobal (stx : Lean.Syntax) (f : Lean.Syntax → Lean.MacroM (Lean.TSyntax `command)) : Lean.MacroM Lean.Syntax

Equations

• Lean.Elab.Command.expandMixfix.withAttrKindGlobal stx f = let attrKind := stx[2]; let stx := stx.setArg 2 Lean.Elab.mkAttrKindGlobal; do let stx ← f stx pure (stx.raw.setArg 2 attrKind)