6 lines
260 B
Text
6 lines
260 B
Text
true : Bool
|
|
true : Bool
|
|
def Bla.bla : Lean.ParserDescr :=
|
|
Lean.ParserDescr.node (Lean.Name.mkStr2 "Bla" "bla") 1022
|
|
(Lean.ParserDescr.binary (Lean.Name.mkStr1 "andthen") (Lean.ParserDescr.symbol "bla")
|
|
(Lean.ParserDescr.cat (Lean.Name.mkStr1 "term") 0))
|