Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Command.expandMixfix.withAttrKindGlobal
(stx : Lean.Syntax)
(f : Lean.Syntax → Lean.MacroM (Lean.TSyntax `command))
:
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)