Init.Notation

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Parser.Syntax.subPrec:

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Parser.Syntax.addPrio:

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.Parser.Syntax.subPrio:

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

source

instance Lean.instCoeTSyntaxSyntax {ks : Lean.SyntaxNodeKinds} :

Coe (Lean.TSyntax ks) Lean.Syntax

Equations

Lean.instCoeTSyntaxSyntax = { coe := fun stx => stx.raw }

source

instance Lean.instCoeSyntaxNodeKindSyntaxNodeKinds:

Coe Lean.SyntaxNodeKind Lean.SyntaxNodeKinds

Equations

Lean.instCoeSyntaxNodeKindSyntaxNodeKinds = { coe := fun k => [k] }

source

def precMax:

Lean.ParserDescr

Equations

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

source

def precArg:

Lean.ParserDescr

Equations

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

source

def precLead:

Lean.ParserDescr

Equations

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

source

def «prec(_)»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def precMin:

Lean.ParserDescr

Equations

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

source

def precMin1:

Lean.ParserDescr

Equations

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

source

def termMax_prec:

Lean.ParserDescr

Equations

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

source

def prioDefault:

Lean.ParserDescr

Equations

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

source

def prioLow:

Lean.ParserDescr

Equations

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

source

def prioMid:

Lean.ParserDescr

Equations

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

source

def prioHigh:

Lean.ParserDescr

Equations

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

source

def «prio(_)»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «stx_+»:

Lean.TrailingParserDescr

Equations

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

source

def «stx_*»:

Lean.TrailingParserDescr

Equations

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

source

def stx_?:

Lean.TrailingParserDescr

Equations

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

source

def «stx_<|>_»:

Lean.TrailingParserDescr

Equations

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

source

def «stx_,*»:

Lean.TrailingParserDescr

Equations

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

source

def «stx_,+»:

Lean.TrailingParserDescr

Equations

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

source

def «stx_,*,?»:

Lean.TrailingParserDescr

Equations

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

source

def «stx_,+,?»:

Lean.TrailingParserDescr

Equations

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

source

def stx!_:

Lean.ParserDescr

Equations

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

source

def rawNatLit:

Lean.ParserDescr

Equations

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

source

def «term_∘_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_×_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_|||_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_^^^_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_&&&_»:

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «term_+_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_-_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_*_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_/_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_%_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<<<_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_>>>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_^_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_++_»:

Lean.TrailingParserDescr

Equations

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

source

def «term-_»:

Lean.ParserDescr

Equations

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

source

def «term~~~_»:

Lean.ParserDescr

Equations

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

source

def «term_<=_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_≤_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_>=_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_≥_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_=_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_==_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_/\_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_∧_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_\/_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_∨_»:

Lean.TrailingParserDescr

Equations

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

source

def «term¬_»:

Lean.ParserDescr

Equations

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

source

def «term_&&_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_||_»:

Lean.TrailingParserDescr

Equations

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

source

def term!_:

Lean.ParserDescr

Equations

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

source

def «term_∈_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_∉_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_::_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<|>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_>>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_>>=_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<*>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<*_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_*>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_<$>_»:

Lean.TrailingParserDescr

Equations

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

source

def termDepIfThenElse:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def termIfThenElse:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «termIfLet_:=_Then_Else_»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def boolIfThenElse:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «term_<|_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_|>_»:

Lean.TrailingParserDescr

Equations

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

source

def «term_$__»:

Lean.TrailingParserDescr

Equations

One or more equations did not get rendered due to their size.

source

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

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def termWithout_expected_type_:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «term[_]»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def «term%[_|_]»:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

def Lean.termThis:

Lean.ParserDescr

Special identifier introduced by "anonymous" have : ..., suffices p ... etc.

Equations

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

source

def Lean.rawStx.quot:

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

source

instance Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStrAnonymousNil:

Coe Lean.Syntax (Lean.TSyntax `rawStx)

Equations

Lean.instCoeSyntaxTSyntaxConsSyntaxNodeKindMkStrAnonymousNil = { coe := fun stx => { raw := stx } }