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.Ext
Std.Internal.Rat
Lean.Data.PersistentHashMap
Lean.Data.PersistentArray
Lean.Data.Xml.Basic
Init.Data.Format.Macro
Init.MacroTrace
Std.Internal.Parsec.Basic
Init.Omega.LinearCombo
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
)
)
)