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 = do let stx_1 ← f (stx.setArg 2 Lean.Elab.mkAttrKindGlobal) pure (stx_1.raw.setArg 2 stx[2])