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