Documentation
Lean
.
Elab
.
Mixfix
Search
Google site search
Lean
.
Elab
.
Mixfix
source
Imports
Init
Lean.Elab.Attributes
Imported by
Lean
.
Elab
.
Command
.
expandMixfix
Lean
.
Elab
.
Command
.
expandMixfix
.
withAttrKindGlobal
source
def
Lean
.
Elab
.
Command
.
expandMixfix
:
Lean.Macro
Instances For
source
def
Lean
.
Elab
.
Command
.
expandMixfix
.
withAttrKindGlobal
(stx :
Lean.Syntax
)
(f :
Lean.Syntax
→
Lean.MacroM
(
Lean.TSyntax
`command
)
)
:
Lean.MacroM
Lean.Syntax
Instances For