Documentation
Init
.
Data
.
ToString
.
Macro
Search
return to top
source
Imports
Init.Meta
Init.Data.ToString.Basic
Imported by
Lean.Data.Json.Basic
Init.Data.ToString
Init.MacroTrace
Init.Ext
Std.Internal.Rat
Init.Omega.LinearCombo
Lean.Data.Xml.Basic
Lean.Data.PersistentHashMap
Std.Internal.Parsec.Basic
Init.Data.Format.Macro
Lean.Data.PersistentArray
termS!_
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
)
)
)