def Lean.Elab.Command.expandMixfix : Macro

Equations

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

def Lean.Elab.Command.expandMixfix.withAttrKindGlobal (stx : Syntax) (f : Syntax → MacroM (TSyntax `command)) : MacroM 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])