Documentation
Lean
.
Elab
.
Mixfix
Search
return to top
source
Imports
Lean.Elab.Attributes
Imported by
Lean.Elab
Lean
.
Elab
.
Command
.
expandMixfix
Lean
.
Elab
.
Command
.
expandMixfix
.
withAttrKindGlobal
source
def
Lean
.
Elab
.
Command
.
expandMixfix
:
Macro
Equations
One or more equations did not get rendered due to their size.
source
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
]
)