Documentation

Init.Notation

def Lean.Parser.Syntax.addPrec :

Lean.TrailingParserDescr

Equations

Lean.Parser.Syntax.addPrec = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.addPrec 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `prec 66))

def Lean.Parser.Syntax.subPrec :

Lean.TrailingParserDescr

Equations

Lean.Parser.Syntax.subPrec = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.subPrec 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `prec 66))

def Lean.Parser.Syntax.addPrio :

Lean.TrailingParserDescr

Equations

Lean.Parser.Syntax.addPrio = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.addPrio 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `prio 66))

def Lean.Parser.Syntax.subPrio :

Lean.TrailingParserDescr

Equations

Lean.Parser.Syntax.subPrio = Lean.ParserDescr.trailingNode `Lean.Parser.Syntax.subPrio 65 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `prio 66))

def precMax :

Lean.ParserDescr

Equations

precMax = Lean.ParserDescr.node `precMax 1024 (Lean.ParserDescr.nonReservedSymbol "max" false)

def precArg :

Lean.ParserDescr

Equations

precArg = Lean.ParserDescr.node `precArg 1024 (Lean.ParserDescr.nonReservedSymbol "arg" false)

def precLead :

Lean.ParserDescr

Equations

precLead = Lean.ParserDescr.node `precLead 1024 (Lean.ParserDescr.nonReservedSymbol "lead" false)

def «prec(_)» :

Lean.ParserDescr

Equations

«prec(_)» = Lean.ParserDescr.node `«prec(_)» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "(" false) (Lean.ParserDescr.cat `prec 0)) (Lean.ParserDescr.symbol ")"))

def precMin :

Lean.ParserDescr

Equations

precMin = Lean.ParserDescr.node `precMin 1024 (Lean.ParserDescr.nonReservedSymbol "min" false)

def precMin1 :

Lean.ParserDescr

Equations

precMin1 = Lean.ParserDescr.node `precMin1 1024 (Lean.ParserDescr.nonReservedSymbol "min1" false)

def termMax_prec :

Lean.ParserDescr

Equations

termMax_prec = Lean.ParserDescr.node `termMax_prec 1024 (Lean.ParserDescr.symbol "max_prec")

def prioDefault :

Lean.ParserDescr

Equations

prioDefault = Lean.ParserDescr.node `prioDefault 1024 (Lean.ParserDescr.nonReservedSymbol "default" false)

def prioLow :

Lean.ParserDescr

Equations

prioLow = Lean.ParserDescr.node `prioLow 1024 (Lean.ParserDescr.nonReservedSymbol "low" false)

def prioMid :

Lean.ParserDescr

Equations

prioMid = Lean.ParserDescr.node `prioMid 1024 (Lean.ParserDescr.nonReservedSymbol "mid" false)

def prioHigh :

Lean.ParserDescr

Equations

prioHigh = Lean.ParserDescr.node `prioHigh 1024 (Lean.ParserDescr.nonReservedSymbol "high" false)

def «prio(_)» :

Lean.ParserDescr

Equations

«prio(_)» = Lean.ParserDescr.node `«prio(_)» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "(" false) (Lean.ParserDescr.cat `prio 0)) (Lean.ParserDescr.symbol ")"))

def «stx_+» :

Lean.TrailingParserDescr

Equations

«stx_+» = Lean.ParserDescr.trailingNode `«stx_+» 1023 1024 (Lean.ParserDescr.symbol "+")

def «stx_*» :

Lean.TrailingParserDescr

Equations

«stx_*» = Lean.ParserDescr.trailingNode `«stx_*» 1023 1024 (Lean.ParserDescr.symbol "*")

def stx_? :

Lean.TrailingParserDescr

Equations

stx_? = Lean.ParserDescr.trailingNode `stx_? 1023 1024 (Lean.ParserDescr.symbol "?")

def «stx_<|>_» :

Lean.TrailingParserDescr

Equations

«stx_<|>_» = Lean.ParserDescr.trailingNode `«stx_<|>_» 2 2 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|> ") (Lean.ParserDescr.cat `stx 1))

def «stx_,*» :

Lean.TrailingParserDescr

Equations

«stx_,*» = Lean.ParserDescr.trailingNode `«stx_,*» 1023 1024 (Lean.ParserDescr.symbol ",*")

def «stx_,+» :

Lean.TrailingParserDescr

Equations

«stx_,+» = Lean.ParserDescr.trailingNode `«stx_,+» 1023 1024 (Lean.ParserDescr.symbol ",+")

def «stx_,*,?» :

Lean.TrailingParserDescr

Equations

«stx_,*,?» = Lean.ParserDescr.trailingNode `«stx_,*,?» 1023 1024 (Lean.ParserDescr.symbol ",*,?")

def «stx_,+,?» :

Lean.TrailingParserDescr

Equations

«stx_,+,?» = Lean.ParserDescr.trailingNode `«stx_,+,?» 1023 1024 (Lean.ParserDescr.symbol ",+,?")

def stx!_ :

Lean.ParserDescr

Equations

stx!_ = Lean.ParserDescr.node `stx!_ 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "!" false) (Lean.ParserDescr.cat `stx 1024))

def rawNatLit :

Lean.ParserDescr

Equations

rawNatLit = Lean.ParserDescr.node `rawNatLit 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "nat_lit ") (Lean.ParserDescr.const `num))

def «term_∘_» :

Lean.TrailingParserDescr

Equations

«term_∘_» = Lean.ParserDescr.trailingNode `«term_∘_» 90 91 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∘ ") (Lean.ParserDescr.cat `term 90))

def «term_×_» :

Lean.TrailingParserDescr

Equations

«term_×_» = Lean.ParserDescr.trailingNode `«term_×_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " × ") (Lean.ParserDescr.cat `term 35))

def «term_|||_» :

Lean.TrailingParserDescr

Equations

«term_|||_» = Lean.ParserDescr.trailingNode `«term_|||_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ||| ") (Lean.ParserDescr.cat `term 56))

def «term_^^^_» :

Lean.TrailingParserDescr

Equations

«term_^^^_» = Lean.ParserDescr.trailingNode `«term_^^^_» 58 58 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^^^ ") (Lean.ParserDescr.cat `term 59))

def «term_&&&_» :

Lean.TrailingParserDescr

Equations

«term_&&&_» = Lean.ParserDescr.trailingNode `«term_&&&_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " &&& ") (Lean.ParserDescr.cat `term 61))

def «term_+_» :

Lean.TrailingParserDescr

Equations

«term_+_» = Lean.ParserDescr.trailingNode `«term_+_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " + ") (Lean.ParserDescr.cat `term 66))

def «term_-_» :

Lean.TrailingParserDescr

Equations

«term_-_» = Lean.ParserDescr.trailingNode `«term_-_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " - ") (Lean.ParserDescr.cat `term 66))

def «term_*_» :

Lean.TrailingParserDescr

Equations

«term_*_» = Lean.ParserDescr.trailingNode `«term_*_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " * ") (Lean.ParserDescr.cat `term 71))

def «term_/_» :

Lean.TrailingParserDescr

Equations

«term_/_» = Lean.ParserDescr.trailingNode `«term_/_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " / ") (Lean.ParserDescr.cat `term 71))

def «term_%_» :

Lean.TrailingParserDescr

Equations

«term_%_» = Lean.ParserDescr.trailingNode `«term_%_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " % ") (Lean.ParserDescr.cat `term 71))

def «term_<<<_» :

Lean.TrailingParserDescr

Equations

«term_<<<_» = Lean.ParserDescr.trailingNode `«term_<<<_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <<< ") (Lean.ParserDescr.cat `term 76))

def «term_>>>_» :

Lean.TrailingParserDescr

Equations

«term_>>>_» = Lean.ParserDescr.trailingNode `«term_>>>_» 75 75 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>> ") (Lean.ParserDescr.cat `term 76))

def «term_^_» :

Lean.TrailingParserDescr

Equations

«term_^_» = Lean.ParserDescr.trailingNode `«term_^_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ ") (Lean.ParserDescr.cat `term 80))

def «term_++_» :

Lean.TrailingParserDescr

Equations

«term_++_» = Lean.ParserDescr.trailingNode `«term_++_» 65 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ++ ") (Lean.ParserDescr.cat `term 66))

def «term-_» :

Lean.ParserDescr

Equations

«term-_» = Lean.ParserDescr.node `«term-_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "-") (Lean.ParserDescr.cat `term 100))

def «term~~~_» :

Lean.ParserDescr

Equations

«term~~~_» = Lean.ParserDescr.node `«term~~~_» 100 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~~~") (Lean.ParserDescr.cat `term 100))

def «term_<=_» :

Lean.TrailingParserDescr

Equations

«term_<=_» = Lean.ParserDescr.trailingNode `«term_<=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <= ") (Lean.ParserDescr.cat `term 51))

def «term_≤_» :

Lean.TrailingParserDescr

Equations

«term_≤_» = Lean.ParserDescr.trailingNode `«term_≤_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ ") (Lean.ParserDescr.cat `term 51))

def «term_<_» :

Lean.TrailingParserDescr

Equations

«term_<_» = Lean.ParserDescr.trailingNode `«term_<_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " < ") (Lean.ParserDescr.cat `term 51))

def «term_>=_» :

Lean.TrailingParserDescr

Equations

«term_>=_» = Lean.ParserDescr.trailingNode `«term_>=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >= ") (Lean.ParserDescr.cat `term 51))

def «term_≥_» :

Lean.TrailingParserDescr

Equations

«term_≥_» = Lean.ParserDescr.trailingNode `«term_≥_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≥ ") (Lean.ParserDescr.cat `term 51))

def «term_>_» :

Lean.TrailingParserDescr

Equations

«term_>_» = Lean.ParserDescr.trailingNode `«term_>_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " > ") (Lean.ParserDescr.cat `term 51))

def «term_=_» :

Lean.TrailingParserDescr

Equations

«term_=_» = Lean.ParserDescr.trailingNode `«term_=_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " = ") (Lean.ParserDescr.cat `term 51))

def «term_==_» :

Lean.TrailingParserDescr

Equations

«term_==_» = Lean.ParserDescr.trailingNode `«term_==_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " == ") (Lean.ParserDescr.cat `term 51))

def «term_/\_» :

Lean.TrailingParserDescr

Equations

«term_/\_» = Lean.ParserDescr.trailingNode `«term_/\_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " /\\ ") (Lean.ParserDescr.cat `term 35))

def «term_∧_» :

Lean.TrailingParserDescr

Equations

«term_∧_» = Lean.ParserDescr.trailingNode `«term_∧_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∧ ") (Lean.ParserDescr.cat `term 35))

def «term_\/_» :

Lean.TrailingParserDescr

Equations

«term_\/_» = Lean.ParserDescr.trailingNode `«term_\/_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " \\/ ") (Lean.ParserDescr.cat `term 30))

def «term_∨_» :

Lean.TrailingParserDescr

Equations

«term_∨_» = Lean.ParserDescr.trailingNode `«term_∨_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∨ ") (Lean.ParserDescr.cat `term 30))

def «term¬_» :

Lean.ParserDescr

Equations

«term¬_» = Lean.ParserDescr.node `«term¬_» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "¬") (Lean.ParserDescr.cat `term 40))

def «term_&&_» :

Lean.TrailingParserDescr

Equations

«term_&&_» = Lean.ParserDescr.trailingNode `«term_&&_» 35 35 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " && ") (Lean.ParserDescr.cat `term 36))

def «term_||_» :

Lean.TrailingParserDescr

Equations

«term_||_» = Lean.ParserDescr.trailingNode `«term_||_» 30 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " || ") (Lean.ParserDescr.cat `term 31))

def term!_ :

Lean.ParserDescr

Equations

term!_ = Lean.ParserDescr.node `term!_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.cat `term 40))

def «term_∈_» :

Lean.TrailingParserDescr

Equations

«term_∈_» = Lean.ParserDescr.trailingNode `«term_∈_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∈ ") (Lean.ParserDescr.cat `term 51))

def «term_∉_» :

Lean.TrailingParserDescr

Equations

«term_∉_» = Lean.ParserDescr.trailingNode `«term_∉_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ∉ ") (Lean.ParserDescr.cat `term 50))

def «term_::_» :

Lean.TrailingParserDescr

Equations

«term_::_» = Lean.ParserDescr.trailingNode `«term_::_» 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 67))

def «term_<|>_» :

Lean.TrailingParserDescr

Equations

«term_<|>_» = Lean.ParserDescr.trailingNode `«term_<|>_» 20 21 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <|> ") (Lean.ParserDescr.cat `term 20))

def «term_>>_» :

Lean.TrailingParserDescr

Equations

«term_>>_» = Lean.ParserDescr.trailingNode `«term_>>_» 60 61 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >> ") (Lean.ParserDescr.cat `term 60))

def «term_>>=_» :

Lean.TrailingParserDescr

Equations

«term_>>=_» = Lean.ParserDescr.trailingNode `«term_>>=_» 55 55 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " >>= ") (Lean.ParserDescr.cat `term 56))

def «term_<*>_» :

Lean.TrailingParserDescr

Equations

«term_<*>_» = Lean.ParserDescr.trailingNode `«term_<*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <*> ") (Lean.ParserDescr.cat `term 61))

def «term_<*_» :

Lean.TrailingParserDescr

Equations

«term_<*_» = Lean.ParserDescr.trailingNode `«term_<*_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <* ") (Lean.ParserDescr.cat `term 61))

def «term_*>_» :

Lean.TrailingParserDescr

Equations

«term_*>_» = Lean.ParserDescr.trailingNode `«term_*>_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " *> ") (Lean.ParserDescr.cat `term 61))

def «term_<$>_» :

Lean.TrailingParserDescr

Equations

«term_<$>_» = Lean.ParserDescr.trailingNode `«term_<$>_» 100 101 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <$> ") (Lean.ParserDescr.cat `term 100))

def termDepIfThenElse :

Lean.ParserDescr

Equations

termDepIfThenElse = Lean.ParserDescr.node `termDepIfThenElse 1022 (Lean.ParserDescr.unary `ppRealGroup (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppIndent (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "if ") (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol " : ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " then"))) (Lean.ParserDescr.const `ppSpace)) (Lean.ParserDescr.cat `term 0))) (Lean.ParserDescr.unary `ppDedent (Lean.ParserDescr.const `ppSpace))) (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "else ") (Lean.ParserDescr.cat `term 0)))))

def termIfThenElse :

Lean.ParserDescr

Equations

termIfThenElse = Lean.ParserDescr.node `termIfThenElse 1022 (Lean.ParserDescr.unary `ppRealGroup (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppIndent (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "if ") (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " then"))) (Lean.ParserDescr.const `ppSpace)) (Lean.ParserDescr.cat `term 0))) (Lean.ParserDescr.unary `ppDedent (Lean.ParserDescr.const `ppSpace))) (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "else ") (Lean.ParserDescr.cat `term 0)))))

def «termIfLet_:=_Then_Else_» :

Lean.ParserDescr

Equations

«termIfLet_:=_Then_Else_» = Lean.ParserDescr.node `«termIfLet_:=_Then_Else_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "if ") (Lean.ParserDescr.symbol "let ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " := ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " then ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " else ")) (Lean.ParserDescr.cat `term 0))

def boolIfThenElse :

Lean.ParserDescr

Equations

boolIfThenElse = Lean.ParserDescr.node `boolIfThenElse 1022 (Lean.ParserDescr.unary `ppRealGroup (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `ppIndent (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bif ") (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " then"))) (Lean.ParserDescr.const `ppSpace)) (Lean.ParserDescr.cat `term 0))) (Lean.ParserDescr.unary `ppDedent (Lean.ParserDescr.const `ppSpace))) (Lean.ParserDescr.unary `ppRealFill (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "else ") (Lean.ParserDescr.cat `term 0)))))

def «term_<|_» :

Lean.TrailingParserDescr

Equations

«term_<|_» = Lean.ParserDescr.trailingNode `«term_<|_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <| ") (Lean.ParserDescr.cat `term 10))

def «term_|>_» :

Lean.TrailingParserDescr

Equations

«term_|>_» = Lean.ParserDescr.trailingNode `«term_|>_» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " |> ") (Lean.ParserDescr.cat `term 11))

def «term_$__» :

Lean.TrailingParserDescr

Equations

«term_$__» = Lean.ParserDescr.trailingNode `«term_$__» 10 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `atomic (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " $") (Lean.ParserDescr.const `ws))) (Lean.ParserDescr.cat `term 10))

def «term{__:_//_}» :

Lean.ParserDescr

Equations

«term{__:_//_}» = Lean.ParserDescr.node `«term{__:_//_}» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{ ") (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " : ") (Lean.ParserDescr.cat `term 0)))) (Lean.ParserDescr.symbol " // ")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol " }"))

def termWithout_expected_type_ :

Lean.ParserDescr

Equations

termWithout_expected_type_ = Lean.ParserDescr.node `termWithout_expected_type_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "without_expected_type ") (Lean.ParserDescr.cat `term 0))

def «term[_]» :

Lean.ParserDescr

Equations

«term[_]» = Lean.ParserDescr.node `«term[_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.cat `term 0) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]"))

def «term%[_|_]» :

Lean.ParserDescr

Equations

«term%[_|_]» = Lean.ParserDescr.node `«term%[_|_]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "%[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.cat `term 0) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "|")) (Lean.ParserDescr.cat `term 0)) (Lean.ParserDescr.symbol "]"))

def Lean.termThis :

Lean.ParserDescr

Equations

Lean.termThis = Lean.ParserDescr.node `Lean.termThis 1024 (Lean.ParserDescr.symbol "this")

Special identifier introduced by "anonymous" have:..., sufficesp... etc.

def Lean.rawStx.quot :

Lean.ParserDescr

Equations

Lean.rawStx.quot = Lean.ParserDescr.node `Lean.Parser.Term.quot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "`(rawStx|") (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `rawStx 0) (Lean.ParserDescr.symbol ")")))