Documentation
Init
.
Data
.
ToString
.
Macro
Search
return to top
source
Imports
Init.Meta
Init.Notation
Imported by
termS!_
← Mathematical handbook
source
def
termS!_
:
Lean.ParserDescr
Equations
termS!_
=
Lean.ParserDescr.node
`termS!_
1024
(
Lean.ParserDescr.binary
`andthen
(
Lean.ParserDescr.symbol
"s!"
)
(
Lean.ParserDescr.unary
`interpolatedStr
(
Lean.ParserDescr.cat
`term
0
)
)
)
Instances For