Lean.Parser.Term

source

def Lean.Parser.Command.commentBody :

Lean.Parser.Parser

Equations

Lean.Parser.Command.commentBody = { info := { collectTokens := id, collectKinds := id, firstTokens := Lean.Parser.FirstTokens.unknown }, fn := Lean.Parser.rawFn (Lean.Parser.finishCommentBlock 1) true }

source

def Lean.Parser.Command.commentBody.parenthesizer :

Lean.PrettyPrinter.Parenthesizer

Equations

Lean.Parser.Command.commentBody.parenthesizer = Lean.PrettyPrinter.Parenthesizer.visitToken

source

def Lean.Parser.Command.commentBody.formatter :

Lean.PrettyPrinter.Formatter

Equations

Lean.Parser.Command.commentBody.formatter = Lean.PrettyPrinter.Formatter.visitAtom Lean.Name.anonymous

source

def Lean.Parser.Command.docComment :

Lean.Parser.Parser

Equations

Lean.Parser.Command.docComment = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "docComment" (some `Lean.Parser.Command.docComment)) (Lean.Parser.leadingNode `Lean.Parser.Command.docComment 1024 (Lean.Parser.ppDedent (HAndThen.hAndThen (Lean.Parser.symbol "/--") fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen Lean.Parser.Command.commentBody fun x => Lean.Parser.ppLine)))

source

@[inline]

def Lean.Parser.tacticParser (rbp : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.tacticParser rbp = Lean.Parser.categoryParser `tactic rbp

source

@[inline]

def Lean.Parser.convParser (rbp : optParam Nat 0) :

Lean.Parser.Parser

Equations

Lean.Parser.convParser rbp = Lean.Parser.categoryParser `conv rbp

source

def Lean.Parser.Tactic.tacticSeq1Indented :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.tacticSeq1Indented = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "tacticSeq1Indented" (some `Lean.Parser.Tactic.tacticSeq1Indented)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.tacticSeq1Indented 1024 (Lean.Parser.many1Indent (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen Lean.Parser.tacticParser fun x => Lean.Parser.optional (Lean.Parser.symbol ";")))))

source

def Lean.Parser.Tactic.tacticSeqBracketed :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.tacticSeqBracketed = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "tacticSeqBracketed" (some `Lean.Parser.Tactic.tacticSeqBracketed)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.tacticSeqBracketed 1024 (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => HAndThen.hAndThen (Lean.Parser.many (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.ppLine fun x => HAndThen.hAndThen Lean.Parser.tacticParser fun x => Lean.Parser.optional (Lean.Parser.symbol ";")))) fun x => Lean.Parser.ppDedent (HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.symbol "}")))

source

def Lean.Parser.Tactic.tacticSeq :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.tacticSeq = Lean.Parser.nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq (HOrElse.hOrElse Lean.Parser.Tactic.tacticSeqBracketed fun x => Lean.Parser.Tactic.tacticSeq1Indented)

source

def Lean.Parser.Tactic.seq1 :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.seq1 = Lean.Parser.node `Lean.Parser.Tactic.seq1 (Lean.Parser.sepBy1 Lean.Parser.tacticParser ";\n" (Lean.Parser.symbol ";\n") true)

source

def Lean.Parser.darrow :

Lean.Parser.Parser

Equations

Lean.Parser.darrow = Lean.Parser.symbol " => "

source

def Lean.Parser.Term.byTactic :

Lean.Parser.Parser

Equations

Lean.Parser.Term.byTactic = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "byTactic" (some `Lean.Parser.Term.byTactic)) (Lean.Parser.leadingNode `Lean.Parser.Term.byTactic Lean.Parser.leadPrec (HAndThen.hAndThen Lean.Parser.ppAllowUngrouped fun x => HAndThen.hAndThen (Lean.Parser.symbol "by ") fun x => Lean.Parser.Tactic.tacticSeq))

source

def Lean.Parser.Term.ident :

Lean.Parser.Parser

Equations

Lean.Parser.Term.ident = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.ident

source

def Lean.Parser.Term.num :

Lean.Parser.Parser

Equations

Lean.Parser.Term.num = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

source

def Lean.Parser.Term.scientific :

Lean.Parser.Parser

Equations

Lean.Parser.Term.scientific = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.scientificLit

source

def Lean.Parser.Term.byTactic' :

Lean.Parser.Parser

Equations

Lean.Parser.Term.byTactic' = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "byTactic'" (some `Lean.Parser.Term.byTactic')) (Lean.Parser.leadingNode `Lean.Parser.Term.byTactic' 1024 (HAndThen.hAndThen (Lean.Parser.symbol "by ") fun x => Lean.Parser.Tactic.tacticSeq))

source

def Lean.Parser.Term.str :

Lean.Parser.Parser

Equations

Lean.Parser.Term.str = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.strLit

source

def Lean.Parser.Term.char :

Lean.Parser.Parser

Equations

Lean.Parser.Term.char = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.charLit

source

def Lean.Parser.Term.optSemicolon (p : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.optSemicolon p = Lean.Parser.ppDedent (HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.symbol ";")) fun x => HAndThen.hAndThen Lean.Parser.ppLine fun x => p)

source

def Lean.Parser.Term.type :

Lean.Parser.Parser

Equations

Lean.Parser.Term.type = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "type" (some `Lean.Parser.Term.type)) (Lean.Parser.leadingNode `Lean.Parser.Term.type 1024 (HAndThen.hAndThen (Lean.Parser.symbol "Type") fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.checkWsBefore "") fun x => HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.leadPrec) fun x => HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.levelParser Lean.Parser.maxPrec)))

source

def Lean.Parser.Term.sort :

Lean.Parser.Parser

Equations

Lean.Parser.Term.sort = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "sort" (some `Lean.Parser.Term.sort)) (Lean.Parser.leadingNode `Lean.Parser.Term.sort 1024 (HAndThen.hAndThen (Lean.Parser.symbol "Sort") fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.checkWsBefore "") fun x => HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.leadPrec) fun x => HAndThen.hAndThen Lean.Parser.checkColGt fun x => Lean.Parser.levelParser Lean.Parser.maxPrec)))

source

def Lean.Parser.Term.prop :

Lean.Parser.Parser

Equations

Lean.Parser.Term.prop = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "prop" (some `Lean.Parser.Term.prop)) (Lean.Parser.leadingNode `Lean.Parser.Term.prop 1024 (Lean.Parser.symbol "Prop"))

source

def Lean.Parser.Term.hole :

Lean.Parser.Parser

Equations

Lean.Parser.Term.hole = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "hole" (some `Lean.Parser.Term.hole)) (Lean.Parser.leadingNode `Lean.Parser.Term.hole 1024 (Lean.Parser.symbol "_"))

source

def Lean.Parser.Term.syntheticHole :

Lean.Parser.Parser

Equations

Lean.Parser.Term.syntheticHole = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "syntheticHole" (some `Lean.Parser.Term.syntheticHole)) (Lean.Parser.leadingNode `Lean.Parser.Term.syntheticHole 1024 (HAndThen.hAndThen (Lean.Parser.symbol "?") fun x => HOrElse.hOrElse Lean.Parser.Term.ident fun x => Lean.Parser.Term.hole))

source

def Lean.Parser.Term.sorry :

Lean.Parser.Parser

Equations

Lean.Parser.Term.sorry = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "sorry" (some `Lean.Parser.Term.sorry)) (Lean.Parser.leadingNode `Lean.Parser.Term.sorry 1024 (Lean.Parser.symbol "sorry"))

source

def Lean.Parser.Term.cdot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.cdot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "cdot" (some `Lean.Parser.Term.cdot)) (Lean.Parser.leadingNode `Lean.Parser.Term.cdot 1024 (HOrElse.hOrElse (Lean.Parser.symbol "·") fun x => Lean.Parser.symbol "."))

source

def Lean.Parser.Term.paren :

Lean.Parser.Parser

Equations

Lean.Parser.Term.paren = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "paren" (some `Lean.Parser.Term.paren)) (Lean.Parser.leadingNode `Lean.Parser.Term.paren 1024 (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.withoutPosition (Lean.Parser.withoutForbidden (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.ppDedentIfGrouped Lean.Parser.termParser) fun x => Lean.Parser.Term.parenSpecial)))) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.anonymousCtor :

Lean.Parser.Parser

Equations

Lean.Parser.Term.anonymousCtor = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "anonymousCtor" (some `Lean.Parser.Term.anonymousCtor)) (Lean.Parser.leadingNode `Lean.Parser.Term.anonymousCtor 1024 (HAndThen.hAndThen (Lean.Parser.symbol "⟨") fun x => HAndThen.hAndThen (Lean.Parser.sepBy Lean.Parser.termParser ", " (Lean.Parser.symbol ", ")) fun x => Lean.Parser.symbol "⟩"))

source

def Lean.Parser.Term.suffices :

Lean.Parser.Parser

Equations

Lean.Parser.Term.suffices = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "suffices" (some `Lean.Parser.Term.suffices)) (Lean.Parser.leadingNode `Lean.Parser.Term.suffices Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "suffices ") fun x => Lean.Parser.Term.sufficesDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.typeAscription :

Lean.Parser.Parser

Equations

Lean.Parser.Term.typeAscription = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "typeAscription" (some `Lean.Parser.Term.typeAscription)) (Lean.Parser.leadingNode `Lean.Parser.Term.typeAscription 1024 (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.show :

Lean.Parser.Parser

Equations

Lean.Parser.Term.show = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "show" (some `Lean.Parser.Term.show)) (Lean.Parser.leadingNode `Lean.Parser.Term.show Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "show ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.showRhs))

source

def Lean.Parser.Term.tupleTail :

Lean.Parser.Parser

Equations

Lean.Parser.Term.tupleTail = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "tupleTail" (some `Lean.Parser.Term.tupleTail)) (Lean.Parser.leadingNode `Lean.Parser.Term.tupleTail 1024 (HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.sepBy1 Lean.Parser.termParser ", " (Lean.Parser.symbol ", ")))

source

def Lean.Parser.Term.parenSpecial :

Lean.Parser.Parser

Equations

Lean.Parser.Term.parenSpecial = Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Term.tupleTail fun x => Lean.Parser.Term.typeAscription)

source

def Lean.Parser.Term.optIdent :

Lean.Parser.Parser

Equations

Lean.Parser.Term.optIdent = Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => Lean.Parser.symbol " : "))

source

def Lean.Parser.Term.fromTerm :

Lean.Parser.Parser

Equations

Lean.Parser.Term.fromTerm = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "fromTerm" (some `Lean.Parser.Term.fromTerm)) (Lean.Parser.leadingNode `Lean.Parser.Term.fromTerm 1024 (HAndThen.hAndThen (Lean.Parser.symbol "from ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.showRhs :

Lean.Parser.Parser

Equations

Lean.Parser.Term.showRhs = HOrElse.hOrElse Lean.Parser.Term.fromTerm fun x => Lean.Parser.Term.byTactic'

source

def Lean.Parser.Term.structInst :

Lean.Parser.Parser

Equations

Lean.Parser.Term.structInst = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInst" (some `Lean.Parser.Term.structInst)) (Lean.Parser.leadingNode `Lean.Parser.Term.structInst 1024 (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => HAndThen.hAndThen Lean.Parser.ppHardSpace fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.termParser ", " (Lean.Parser.symbol ", ")) fun x => Lean.Parser.symbol " with "))) fun x => HAndThen.hAndThen (Lean.Parser.manyIndent (Lean.Parser.group (HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.Term.structInstFieldAbbrev fun x => Lean.Parser.Term.structInstField) fun x => Lean.Parser.optional (Lean.Parser.symbol ", ")))) fun x => HAndThen.hAndThen Lean.Parser.Term.optEllipsis fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser)) fun x => Lean.Parser.symbol " }"))

source

def Lean.Parser.Term.sufficesDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.sufficesDecl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "sufficesDecl" (some `Lean.Parser.Term.sufficesDecl)) (Lean.Parser.leadingNode `Lean.Parser.Term.sufficesDecl 1024 (HAndThen.hAndThen Lean.Parser.Term.optIdent fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.showRhs))

source

def Lean.Parser.Term.structInstArrayRef :

Lean.Parser.Parser

Equations

Lean.Parser.Term.structInstArrayRef = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInstArrayRef" (some `Lean.Parser.Term.structInstArrayRef)) (Lean.Parser.leadingNode `Lean.Parser.Term.structInstArrayRef 1024 (HAndThen.hAndThen (Lean.Parser.symbol "[") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.symbol "]"))

source

def Lean.Parser.Term.structInstLVal :

Lean.Parser.Parser

Equations

Lean.Parser.Term.structInstLVal = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInstLVal" (some `Lean.Parser.Term.structInstLVal)) (Lean.Parser.leadingNode `Lean.Parser.Term.structInstLVal 1024 (HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.Term.ident fun x => HOrElse.hOrElse Lean.Parser.fieldIdx fun x => Lean.Parser.Term.structInstArrayRef) fun x => Lean.Parser.many (HOrElse.hOrElse (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol ".") fun x => HOrElse.hOrElse Lean.Parser.Term.ident fun x => Lean.Parser.fieldIdx)) fun x => Lean.Parser.Term.structInstArrayRef)))

source

def Lean.Parser.Term.structInstField :

Lean.Parser.Parser

Equations

Lean.Parser.Term.structInstField = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInstField" (some `Lean.Parser.Term.structInstField)) (Lean.Parser.leadingNode `Lean.Parser.Term.structInstField 1024 (HAndThen.hAndThen Lean.Parser.Term.structInstLVal fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => Lean.Parser.termParser)))

source

def Lean.Parser.Term.explicit :

Lean.Parser.Parser

Equations

Lean.Parser.Term.explicit = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "explicit" (some `Lean.Parser.Term.explicit)) (Lean.Parser.leadingNode `Lean.Parser.Term.explicit 1024 (HAndThen.hAndThen (Lean.Parser.symbol "@") fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.structInstFieldAbbrev :

Lean.Parser.Parser

Equations

Lean.Parser.Term.structInstFieldAbbrev = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "structInstFieldAbbrev" (some `Lean.Parser.Term.structInstFieldAbbrev)) (Lean.Parser.leadingNode `Lean.Parser.Term.structInstFieldAbbrev 1024 (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => Lean.Parser.notFollowedBy (HOrElse.hOrElse (Lean.Parser.symbol ".") fun x => HOrElse.hOrElse (Lean.Parser.symbol ":=") fun x => Lean.Parser.symbol "[") "invalid field abbreviation")))

source

def Lean.Parser.Term.inaccessible :

Lean.Parser.Parser

Equations

Lean.Parser.Term.inaccessible = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "inaccessible" (some `Lean.Parser.Term.inaccessible)) (Lean.Parser.leadingNode `Lean.Parser.Term.inaccessible 1024 (HAndThen.hAndThen (Lean.Parser.symbol ".(") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.optEllipsis :

Lean.Parser.Parser

Equations

Lean.Parser.Term.optEllipsis = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "optEllipsis" (some `Lean.Parser.Term.optEllipsis)) (Lean.Parser.leadingNode `Lean.Parser.Term.optEllipsis 1024 (Lean.Parser.optional (Lean.Parser.symbol "..")))

source

def Lean.Parser.Term.typeSpec :

Lean.Parser.Parser

Equations

Lean.Parser.Term.typeSpec = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "typeSpec" (some `Lean.Parser.Term.typeSpec)) (Lean.Parser.leadingNode `Lean.Parser.Term.typeSpec 1024 (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.optType :

Lean.Parser.Parser

Equations

Lean.Parser.Term.optType = Lean.Parser.optional Lean.Parser.Term.typeSpec

source

def Lean.Parser.Term.binderIdent :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binderIdent = HOrElse.hOrElse Lean.Parser.Term.ident fun x => Lean.Parser.Term.hole

source

def Lean.Parser.Term.binderType (requireType : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binderType requireType = if requireType = true then Lean.Parser.node Lean.nullKind (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser) else Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.binderTactic :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binderTactic = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binderTactic" (some `Lean.Parser.Term.binderTactic)) (Lean.Parser.leadingNode `Lean.Parser.Term.binderTactic 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => Lean.Parser.symbol " by ")) fun x => Lean.Parser.Tactic.tacticSeq))

source

def Lean.Parser.Term.binderDefault :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binderDefault = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binderDefault" (some `Lean.Parser.Term.binderDefault)) (Lean.Parser.leadingNode `Lean.Parser.Term.binderDefault 1024 (HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.explicitBinder (requireType : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.explicitBinder requireType = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "explicitBinder" (some `Lean.Parser.Term.explicitBinder)) (Lean.Parser.leadingNode `Lean.Parser.Term.explicitBinder 1024 (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => HAndThen.hAndThen (Lean.Parser.Term.binderType requireType) fun x => HAndThen.hAndThen (Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Term.binderTactic fun x => Lean.Parser.Term.binderDefault)) fun x => Lean.Parser.symbol ")")))

source

def Lean.Parser.Term.implicitBinder (requireType : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.implicitBinder requireType = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "implicitBinder" (some `Lean.Parser.Term.implicitBinder)) (Lean.Parser.leadingNode `Lean.Parser.Term.implicitBinder 1024 (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => HAndThen.hAndThen (Lean.Parser.Term.binderType requireType) fun x => Lean.Parser.symbol "}")))

source

def Lean.Parser.Term.strictImplicitLeftBracket :

Lean.Parser.Parser

Equations

Lean.Parser.Term.strictImplicitLeftBracket = HOrElse.hOrElse (Lean.Parser.atomic (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => Lean.Parser.symbol "{"))) fun x => Lean.Parser.symbol "⦃"

source

def Lean.Parser.Term.strictImplicitRightBracket :

Lean.Parser.Parser

Equations

Lean.Parser.Term.strictImplicitRightBracket = HOrElse.hOrElse (Lean.Parser.atomic (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol "}") fun x => Lean.Parser.symbol "}"))) fun x => Lean.Parser.symbol "⦄"

source

def Lean.Parser.Term.strictImplicitBinder (requireType : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.strictImplicitBinder requireType = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "strictImplicitBinder" (some `Lean.Parser.Term.strictImplicitBinder)) (Lean.Parser.leadingNode `Lean.Parser.Term.strictImplicitBinder 1024 (HAndThen.hAndThen Lean.Parser.Term.strictImplicitLeftBracket fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => HAndThen.hAndThen (Lean.Parser.Term.binderType requireType) fun x => Lean.Parser.Term.strictImplicitRightBracket)))

source

def Lean.Parser.Term.instBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.instBinder = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "instBinder" (some `Lean.Parser.Term.instBinder)) (Lean.Parser.leadingNode `Lean.Parser.Term.instBinder 1024 (HAndThen.hAndThen (Lean.Parser.symbol "[") fun x => HAndThen.hAndThen Lean.Parser.Term.optIdent fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.symbol "]")))

source

def Lean.Parser.Term.bracketedBinder (requireType : optParam Bool false) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.bracketedBinder requireType = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "bracketedBinder" none false) (HOrElse.hOrElse (Lean.Parser.Term.explicitBinder requireType) fun x => HOrElse.hOrElse (Lean.Parser.Term.strictImplicitBinder requireType) fun x => HOrElse.hOrElse (Lean.Parser.Term.implicitBinder requireType) fun x => Lean.Parser.Term.instBinder)

source

def Lean.Parser.Term.depArrow :

Lean.Parser.Parser

Equations

Lean.Parser.Term.depArrow = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "depArrow" (some `Lean.Parser.Term.depArrow)) (Lean.Parser.leadingNode `Lean.Parser.Term.depArrow 25 (HAndThen.hAndThen (Lean.Parser.Term.bracketedBinder true) fun x => HAndThen.hAndThen (Lean.Parser.unicodeSymbol " → " " -> ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.forall :

Lean.Parser.Parser

Equations

Lean.Parser.Term.forall = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "forall" (some `Lean.Parser.Term.forall)) (Lean.Parser.leadingNode `Lean.Parser.Term.forall Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.unicodeSymbol "∀" "forall") fun x => HAndThen.hAndThen (Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => HOrElse.hOrElse Lean.Parser.Term.simpleBinder fun x => Lean.Parser.Term.bracketedBinder)) fun x => HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.simpleBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.simpleBinder = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "simpleBinder" (some `Lean.Parser.Term.simpleBinder)) (Lean.Parser.leadingNode `Lean.Parser.Term.simpleBinder 1024 (HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => Lean.Parser.Term.optType))

source

def Lean.Parser.Term.matchAlt (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchAlt rhsParser = Lean.Parser.nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt (HAndThen.hAndThen (Lean.Parser.symbol "| ") fun x => Lean.Parser.ppIndent (HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.termParser ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => HAndThen.hAndThen (Lean.Parser.checkColGe "alternative right-hand-side to start in a column greater than or equal to the corresponding '|'") fun x => rhsParser))

source

def Lean.Parser.Term.matchAltExpr :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchAltExpr = Lean.Parser.Term.matchAlt

source

def Lean.Parser.Term.match :

Lean.Parser.Parser

Equations

Lean.Parser.Term.match = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "match" (some `Lean.Parser.Term.match)) (Lean.Parser.leadingNode `Lean.Parser.Term.match Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "match ") fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Term.generalizingParam) fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.Term.matchDiscr ", " (Lean.Parser.symbol ", ")) fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => HAndThen.hAndThen (Lean.Parser.symbol " with ") fun x => Lean.Parser.ppDedent Lean.Parser.Term.matchAlts))

source

def Lean.Parser.Term.matchAlts (rhsParser : optParam Lean.Parser.Parser Lean.Parser.termParser) :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchAlts rhsParser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "matchAlts" (some `Lean.Parser.Term.matchAlts)) (Lean.Parser.leadingNode `Lean.Parser.Term.matchAlts 1024 (Lean.Parser.withPosition (Lean.Parser.many1Indent (HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.Term.matchAlt rhsParser))))

source

def Lean.Parser.Term.nomatch :

Lean.Parser.Parser

Equations

Lean.Parser.Term.nomatch = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "nomatch" (some `Lean.Parser.Term.nomatch)) (Lean.Parser.leadingNode `Lean.Parser.Term.nomatch Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "nomatch ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.matchDiscr :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchDiscr = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "matchDiscr" (some `Lean.Parser.Term.matchDiscr)) (Lean.Parser.leadingNode `Lean.Parser.Term.matchDiscr 1024 (HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "no space before ':'") fun x => Lean.Parser.symbol ":"))) fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.trueVal :

Lean.Parser.Parser

Equations

Lean.Parser.Term.trueVal = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "trueVal" (some `Lean.Parser.Term.trueVal)) (Lean.Parser.leadingNode `Lean.Parser.Term.trueVal 1024 (Lean.Parser.nonReservedSymbol "true"))

source

def Lean.Parser.Term.falseVal :

Lean.Parser.Parser

Equations

Lean.Parser.Term.falseVal = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "falseVal" (some `Lean.Parser.Term.falseVal)) (Lean.Parser.leadingNode `Lean.Parser.Term.falseVal 1024 (Lean.Parser.nonReservedSymbol "false"))

source

def Lean.Parser.Term.generalizingParam :

Lean.Parser.Parser

Equations

Lean.Parser.Term.generalizingParam = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "generalizingParam" (some `Lean.Parser.Term.generalizingParam)) (Lean.Parser.leadingNode `Lean.Parser.Term.generalizingParam 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => Lean.Parser.nonReservedSymbol "generalizing")) fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.Term.trueVal fun x => Lean.Parser.Term.falseVal) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.fun :

Lean.Parser.Parser

Equations

Lean.Parser.Term.fun = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "fun" (some `Lean.Parser.Term.fun)) (Lean.Parser.leadingNode `Lean.Parser.Term.fun Lean.Parser.maxPrec (HAndThen.hAndThen Lean.Parser.ppAllowUngrouped fun x => HAndThen.hAndThen (Lean.Parser.unicodeSymbol "λ" "fun") fun x => HOrElse.hOrElse Lean.Parser.Term.basicFun fun x => Lean.Parser.Term.matchAlts))

source

def Lean.Parser.Term.leading_parser :

Lean.Parser.Parser

Equations

Lean.Parser.Term.leading_parser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "leading_parser" (some `Lean.Parser.Term.leading_parser)) (Lean.Parser.leadingNode `Lean.Parser.Term.leading_parser Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "leading_parser ") fun x => HAndThen.hAndThen Lean.Parser.Term.optExprPrecedence fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.funImplicitBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.funImplicitBinder = HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.lookahead (HAndThen.hAndThen (Lean.Parser.symbol "{") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => HOrElse.hOrElse (Lean.Parser.symbol " : ") fun x => Lean.Parser.symbol "}"))) fun x => Lean.Parser.Term.implicitBinder

source

def Lean.Parser.Term.funStrictImplicitBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.funStrictImplicitBinder = HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.lookahead (HAndThen.hAndThen Lean.Parser.Term.strictImplicitLeftBracket fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => HOrElse.hOrElse (Lean.Parser.symbol " : ") fun x => Lean.Parser.Term.strictImplicitRightBracket))) fun x => Lean.Parser.Term.strictImplicitBinder

source

def Lean.Parser.Term.trailing_parser :

Lean.Parser.Parser

Equations

Lean.Parser.Term.trailing_parser = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "trailing_parser" (some `Lean.Parser.Term.trailing_parser)) (Lean.Parser.leadingNode `Lean.Parser.Term.trailing_parser Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "trailing_parser ") fun x => HAndThen.hAndThen Lean.Parser.Term.optExprPrecedence fun x => HAndThen.hAndThen Lean.Parser.Term.optExprPrecedence fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.funSimpleBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.funSimpleBinder = HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.lookahead (HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => Lean.Parser.symbol " : "))) fun x => Lean.Parser.Term.simpleBinder

source

def Lean.Parser.Term.borrowed :

Lean.Parser.Parser

Equations

Lean.Parser.Term.borrowed = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "borrowed" (some `Lean.Parser.Term.borrowed)) (Lean.Parser.leadingNode `Lean.Parser.Term.borrowed 1024 (HAndThen.hAndThen (Lean.Parser.symbol "@& ") fun x => Lean.Parser.termParser Lean.Parser.leadPrec))

source

def Lean.Parser.Term.funBinder :

Lean.Parser.Parser

Equations

Lean.Parser.Term.funBinder = HOrElse.hOrElse Lean.Parser.Term.funStrictImplicitBinder fun x => HOrElse.hOrElse Lean.Parser.Term.funImplicitBinder fun x => HOrElse.hOrElse Lean.Parser.Term.instBinder fun x => HOrElse.hOrElse Lean.Parser.Term.funSimpleBinder fun x => Lean.Parser.termParser Lean.Parser.maxPrec

source

def Lean.Parser.Term.quotedName :

Lean.Parser.Parser

Equations

Lean.Parser.Term.quotedName = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quotedName" (some `Lean.Parser.Term.quotedName)) (Lean.Parser.leadingNode `Lean.Parser.Term.quotedName 1024 Lean.Parser.nameLit)

source

def Lean.Parser.Term.basicFun :

Lean.Parser.Parser

Equations

Lean.Parser.Term.basicFun = Lean.Parser.nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (HAndThen.hAndThen (Lean.Parser.ppGroup (HAndThen.hAndThen (Lean.Parser.many1 (HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.Term.funBinder)) fun x => Lean.Parser.symbol " =>")) fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.doubleQuotedName :

Lean.Parser.Parser

Equations

Lean.Parser.Term.doubleQuotedName = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "doubleQuotedName" (some `Lean.Parser.Term.doubleQuotedName)) (Lean.Parser.leadingNode `Lean.Parser.Term.doubleQuotedName 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`") fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.rawCh (Char.ofNat 96)) fun x => Lean.Parser.Term.ident))

source

def Lean.Parser.Term.optExprPrecedence :

Lean.Parser.Parser

Equations

Lean.Parser.Term.optExprPrecedence = Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.atomic (Lean.Parser.symbol ":")) fun x => Lean.Parser.termParser Lean.Parser.maxPrec)

source

def Lean.Parser.Term.simpleBinderWithoutType :

Lean.Parser.Parser

Equations

Lean.Parser.Term.simpleBinderWithoutType = Lean.Parser.nodeWithAntiquot "simpleBinder" `Lean.Parser.Term.simpleBinder (HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Term.binderIdent) fun x => Lean.Parser.pushNone) true

source

def Lean.Parser.Term.let :

Lean.Parser.Parser

Equations

Lean.Parser.Term.let = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "let" (some `Lean.Parser.Term.let)) (Lean.Parser.leadingNode `Lean.Parser.Term.let Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => Lean.Parser.Term.letDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.let_fun :

Lean.Parser.Parser

Equations

Lean.Parser.Term.let_fun = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "let_fun" (some `Lean.Parser.Term.let_fun)) (Lean.Parser.leadingNode `Lean.Parser.Term.let_fun Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (HOrElse.hOrElse (Lean.Parser.symbol "let_fun ") fun x => Lean.Parser.symbol "let_λ") fun x => Lean.Parser.Term.letDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.let_delayed :

Lean.Parser.Parser

Equations

Lean.Parser.Term.let_delayed = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "let_delayed" (some `Lean.Parser.Term.let_delayed)) (Lean.Parser.leadingNode `Lean.Parser.Term.let_delayed Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "let_delayed ") fun x => Lean.Parser.Term.letDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.letIdLhs :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letIdLhs = HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.notFollowedBy (HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "") fun x => Lean.Parser.symbol "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`") fun x => HAndThen.hAndThen (Lean.Parser.many (HAndThen.hAndThen Lean.Parser.ppSpace fun x => HOrElse.hOrElse Lean.Parser.Term.simpleBinderWithoutType fun x => Lean.Parser.Term.bracketedBinder)) fun x => Lean.Parser.Term.optType

source

def Lean.Parser.Term.let_tmp :

Lean.Parser.Parser

Equations

Lean.Parser.Term.let_tmp = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "let_tmp" (some `Lean.Parser.Term.let_tmp)) (Lean.Parser.leadingNode `Lean.Parser.Term.let_tmp Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "let_tmp ") fun x => Lean.Parser.Term.letDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.letIdDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letIdDecl = Lean.Parser.nodeWithAntiquot "letIdDecl" `Lean.Parser.Term.letIdDecl (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.letIdLhs fun x => Lean.Parser.symbol " := ")) fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.letPatDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letPatDecl = Lean.Parser.nodeWithAntiquot "letPatDecl" `Lean.Parser.Term.letPatDecl (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen Lean.Parser.pushNone fun x => HAndThen.hAndThen Lean.Parser.Term.optType fun x => Lean.Parser.symbol " := ")) fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.have :

Lean.Parser.Parser

Equations

Lean.Parser.Term.have = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "have" (some `Lean.Parser.Term.have)) (Lean.Parser.leadingNode `Lean.Parser.Term.have Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "have ") fun x => Lean.Parser.Term.haveDecl)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.letEqnsDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letEqnsDecl = Lean.Parser.nodeWithAntiquot "letEqnsDecl" `Lean.Parser.Term.letEqnsDecl (HAndThen.hAndThen Lean.Parser.Term.letIdLhs fun x => HOrElse.hOrElse (Lean.Parser.symbol " := ") fun x => Lean.Parser.Term.matchAlts)

source

def Lean.Parser.Term.letDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letDecl = Lean.Parser.nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (HAndThen.hAndThen (Lean.Parser.notFollowedBy (Lean.Parser.nonReservedSymbol "rec") "rec") fun x => HOrElse.hOrElse Lean.Parser.Term.letIdDecl fun x => HOrElse.hOrElse Lean.Parser.Term.letPatDecl fun x => Lean.Parser.Term.letEqnsDecl)

source

def Lean.Parser.Term.letrec :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letrec = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "letrec" (some `Lean.Parser.Term.letrec)) (Lean.Parser.leadingNode `Lean.Parser.Term.letrec Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.group (HAndThen.hAndThen (Lean.Parser.symbol "let ") fun x => Lean.Parser.nonReservedSymbol "rec ")) fun x => Lean.Parser.Term.letRecDecls)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.haveIdLhs :

Lean.Parser.Parser

Equations

Lean.Parser.Term.haveIdLhs = HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen Lean.Parser.Term.ident fun x => Lean.Parser.many (HAndThen.hAndThen Lean.Parser.ppSpace fun x => HOrElse.hOrElse Lean.Parser.Term.simpleBinderWithoutType fun x => Lean.Parser.Term.bracketedBinder))) fun x => Lean.Parser.Term.optType

source

def Lean.Parser.Term.noindex :

Lean.Parser.Parser

Equations

Lean.Parser.Term.noindex = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "noindex" (some `Lean.Parser.Term.noindex)) (Lean.Parser.leadingNode `Lean.Parser.Term.noindex 1024 (HAndThen.hAndThen (Lean.Parser.symbol "no_index ") fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.haveIdDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.haveIdDecl = Lean.Parser.nodeWithAntiquot "haveIdDecl" `Lean.Parser.Term.haveIdDecl (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.haveIdLhs fun x => Lean.Parser.symbol " := ")) fun x => Lean.Parser.termParser)

source

def Lean.Parser.Term.haveEqnsDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.haveEqnsDecl = Lean.Parser.nodeWithAntiquot "haveEqnsDecl" `Lean.Parser.Term.haveEqnsDecl (HAndThen.hAndThen Lean.Parser.Term.haveIdLhs fun x => Lean.Parser.Term.matchAlts)

source

def Lean.Parser.Term.binrel :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binrel = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binrel" (some `Lean.Parser.Term.binrel)) (Lean.Parser.leadingNode `Lean.Parser.Term.binrel 1024 (HAndThen.hAndThen (Lean.Parser.symbol "binrel% ") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.haveDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.haveDecl = Lean.Parser.nodeWithAntiquot "haveDecl" `Lean.Parser.Term.haveDecl (HOrElse.hOrElse Lean.Parser.Term.haveIdDecl fun x => HOrElse.hOrElse Lean.Parser.Term.letPatDecl fun x => Lean.Parser.Term.haveEqnsDecl)

source

def Lean.Parser.Term.binrel_no_prop :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binrel_no_prop = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binrel_no_prop" (some `Lean.Parser.Term.binrel_no_prop)) (Lean.Parser.leadingNode `Lean.Parser.Term.binrel_no_prop 1024 (HAndThen.hAndThen (Lean.Parser.symbol "binrel_no_prop% ") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.scoped :

Lean.Parser.Parser

Equations

Lean.Parser.Term.scoped = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "scoped" (some `Lean.Parser.Term.scoped)) (Lean.Parser.leadingNode `Lean.Parser.Term.scoped 1024 (Lean.Parser.symbol "scoped "))

source

def Lean.Parser.Term.binop :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binop = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binop" (some `Lean.Parser.Term.binop)) (Lean.Parser.leadingNode `Lean.Parser.Term.binop 1024 (HAndThen.hAndThen (Lean.Parser.symbol "binop% ") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.binop_lazy :

Lean.Parser.Parser

Equations

Lean.Parser.Term.binop_lazy = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binop_lazy" (some `Lean.Parser.Term.binop_lazy)) (Lean.Parser.leadingNode `Lean.Parser.Term.binop_lazy 1024 (HAndThen.hAndThen (Lean.Parser.symbol "binop_lazy% ") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.local :

Lean.Parser.Parser

Equations

Lean.Parser.Term.local = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "local" (some `Lean.Parser.Term.local)) (Lean.Parser.leadingNode `Lean.Parser.Term.local 1024 (Lean.Parser.symbol "local "))

source

def Lean.Parser.Term.attrKind :

Lean.Parser.Parser

Equations

Lean.Parser.Term.attrKind = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "attrKind" (some `Lean.Parser.Term.attrKind)) (Lean.Parser.leadingNode `Lean.Parser.Term.attrKind 1024 (Lean.Parser.optional (HOrElse.hOrElse Lean.Parser.Term.scoped fun x => Lean.Parser.Term.local)))

source

def Lean.Parser.Term.attrInstance :

Lean.Parser.Parser

Equations

Lean.Parser.Term.attrInstance = Lean.Parser.ppGroup (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "attrInstance" (some `Lean.Parser.Term.attrInstance)) (Lean.Parser.leadingNode `Lean.Parser.Term.attrInstance 1024 (HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => Lean.Parser.attrParser)))

source

def Lean.Parser.Term.forInMacro :

Lean.Parser.Parser

Equations

Lean.Parser.Term.forInMacro = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "forInMacro" (some `Lean.Parser.Term.forInMacro)) (Lean.Parser.leadingNode `Lean.Parser.Term.forInMacro 1024 (HAndThen.hAndThen (Lean.Parser.symbol "for_in% ") fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.attributes :

Lean.Parser.Parser

Equations

Lean.Parser.Term.attributes = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "attributes" (some `Lean.Parser.Term.attributes)) (Lean.Parser.leadingNode `Lean.Parser.Term.attributes 1024 (HAndThen.hAndThen (Lean.Parser.symbol "@[") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.Term.attrInstance ", " (Lean.Parser.symbol ", ")) fun x => Lean.Parser.symbol "]"))

source

def Lean.Parser.Term.typeOf :

Lean.Parser.Parser

Equations

Lean.Parser.Term.typeOf = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "typeOf" (some `Lean.Parser.Term.typeOf)) (Lean.Parser.leadingNode `Lean.Parser.Term.typeOf 1024 (HAndThen.hAndThen (Lean.Parser.symbol "type_of% ") fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.letRecDecl :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letRecDecl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "letRecDecl" (some `Lean.Parser.Term.letRecDecl)) (Lean.Parser.leadingNode `Lean.Parser.Term.letRecDecl 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Term.attributes) fun x => Lean.Parser.Term.letDecl))

source

def Lean.Parser.Term.ensureTypeOf :

Lean.Parser.Parser

Equations

Lean.Parser.Term.ensureTypeOf = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ensureTypeOf" (some `Lean.Parser.Term.ensureTypeOf)) (Lean.Parser.leadingNode `Lean.Parser.Term.ensureTypeOf 1024 (HAndThen.hAndThen (Lean.Parser.symbol "ensure_type_of% ") fun x => HAndThen.hAndThen (Lean.Parser.termParser Lean.Parser.maxPrec) fun x => HAndThen.hAndThen Lean.Parser.strLit fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.letRecDecls :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letRecDecls = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "letRecDecls" (some `Lean.Parser.Term.letRecDecls)) (Lean.Parser.leadingNode `Lean.Parser.Term.letRecDecls 1024 (Lean.Parser.sepBy1 Lean.Parser.Term.letRecDecl ", " (Lean.Parser.symbol ", ")))

source

def Lean.Parser.Term.ensureExpectedType :

Lean.Parser.Parser

Equations

Lean.Parser.Term.ensureExpectedType = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ensureExpectedType" (some `Lean.Parser.Term.ensureExpectedType)) (Lean.Parser.leadingNode `Lean.Parser.Term.ensureExpectedType 1024 (HAndThen.hAndThen (Lean.Parser.symbol "ensure_expected_type% ") fun x => HAndThen.hAndThen Lean.Parser.strLit fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.noImplicitLambda :

Lean.Parser.Parser

Equations

Lean.Parser.Term.noImplicitLambda = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "noImplicitLambda" (some `Lean.Parser.Term.noImplicitLambda)) (Lean.Parser.leadingNode `Lean.Parser.Term.noImplicitLambda 1024 (HAndThen.hAndThen (Lean.Parser.symbol "no_implicit_lambda% ") fun x => Lean.Parser.termParser Lean.Parser.maxPrec))

source

def Lean.Parser.Term.letMVar :

Lean.Parser.Parser

Equations

Lean.Parser.Term.letMVar = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "letMVar" (some `Lean.Parser.Term.letMVar)) (Lean.Parser.leadingNode `Lean.Parser.Term.letMVar 1024 (HAndThen.hAndThen (Lean.Parser.symbol "let_mvar% ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "?") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => HAndThen.hAndThen (Lean.Parser.symbol "; ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.waitIfTypeMVar :

Lean.Parser.Parser

Equations

Lean.Parser.Term.waitIfTypeMVar = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "waitIfTypeMVar" (some `Lean.Parser.Term.waitIfTypeMVar)) (Lean.Parser.leadingNode `Lean.Parser.Term.waitIfTypeMVar 1024 (HAndThen.hAndThen (Lean.Parser.symbol "wait_if_type_mvar% ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "?") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol "; ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.waitIfTypeContainsMVar :

Lean.Parser.Parser

Equations

Lean.Parser.Term.waitIfTypeContainsMVar = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "waitIfTypeContainsMVar" (some `Lean.Parser.Term.waitIfTypeContainsMVar)) (Lean.Parser.leadingNode `Lean.Parser.Term.waitIfTypeContainsMVar 1024 (HAndThen.hAndThen (Lean.Parser.symbol "wait_if_type_contains_mvar% ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "?") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol "; ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.whereDecls :

Lean.Parser.Parser

Equations

Lean.Parser.Term.whereDecls = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "whereDecls" (some `Lean.Parser.Term.whereDecls)) (Lean.Parser.leadingNode `Lean.Parser.Term.whereDecls 1024 (HAndThen.hAndThen (Lean.Parser.symbol " where") fun x => Lean.Parser.many1Indent (HAndThen.hAndThen Lean.Parser.ppLine fun x => Lean.Parser.ppGroup (Lean.Parser.group (HAndThen.hAndThen Lean.Parser.Term.letRecDecl fun x => Lean.Parser.optional (Lean.Parser.symbol ";"))))))

source

def Lean.Parser.Term.waitIfContainsMVar :

Lean.Parser.Parser

Equations

Lean.Parser.Term.waitIfContainsMVar = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "waitIfContainsMVar" (some `Lean.Parser.Term.waitIfContainsMVar)) (Lean.Parser.leadingNode `Lean.Parser.Term.waitIfContainsMVar 1024 (HAndThen.hAndThen (Lean.Parser.symbol "wait_if_contains_mvar% ") fun x => HAndThen.hAndThen (Lean.Parser.symbol "?") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol "; ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.matchAltsWhereDecls :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchAltsWhereDecls = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "matchAltsWhereDecls" (some `Lean.Parser.Term.matchAltsWhereDecls)) (Lean.Parser.leadingNode `Lean.Parser.Term.matchAltsWhereDecls 1024 (HAndThen.hAndThen Lean.Parser.Term.matchAlts fun x => Lean.Parser.optional Lean.Parser.Term.whereDecls))

source

def Lean.Parser.Term.app :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.app = Lean.Parser.trailingNode `Lean.Parser.Term.app Lean.Parser.leadPrec Lean.Parser.maxPrec (Lean.Parser.many1 Lean.Parser.Term.argument)

source

def Lean.Parser.Term.proj :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.proj = Lean.Parser.trailingNode `Lean.Parser.Term.proj 1024 0 (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.symbol ".") fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HOrElse.hOrElse Lean.Parser.fieldIdx fun x => Lean.Parser.Term.ident)

source

def Lean.Parser.Term.completion :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.completion = Lean.Parser.trailingNode `Lean.Parser.Term.completion 1024 0 (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => Lean.Parser.symbol ".")

source

def Lean.Parser.Term.arrayRef :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.arrayRef = Lean.Parser.trailingNode `Lean.Parser.Term.arrayRef 1024 0 (HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.symbol "[") fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.symbol "]")

source

def Lean.Parser.Term.arrow :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.arrow = Lean.Parser.trailingNode `Lean.Parser.Term.arrow 1024 0 (HAndThen.hAndThen (Lean.Parser.checkPrec 25) fun x => HAndThen.hAndThen (Lean.Parser.unicodeSymbol " → " " -> ") fun x => Lean.Parser.termParser 25)

source

def Lean.Parser.Term.explicitUniv :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.explicitUniv = Lean.Parser.trailingNode `Lean.Parser.Term.explicitUniv 1024 0 (HAndThen.hAndThen (Lean.Parser.checkStackTop Lean.Parser.Term.isIdent "expected preceding identifier") fun x => HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "no space before '.{'") fun x => HAndThen.hAndThen (Lean.Parser.symbol ".{") fun x => HAndThen.hAndThen (Lean.Parser.sepBy1 Lean.Parser.levelParser ", " (Lean.Parser.symbol ", ")) fun x => Lean.Parser.symbol "}")

source

def Lean.Parser.Term.namedPattern :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.namedPattern = Lean.Parser.trailingNode `Lean.Parser.Term.namedPattern 1024 0 (HAndThen.hAndThen (Lean.Parser.checkStackTop Lean.Parser.Term.isIdent "expected preceding identifier") fun x => HAndThen.hAndThen (Lean.Parser.checkNoWsBefore "no space before '@'") fun x => HAndThen.hAndThen (Lean.Parser.symbol "@") fun x => HAndThen.hAndThen (Lean.Parser.optional (Lean.Parser.atomic (HAndThen.hAndThen Lean.Parser.Term.ident fun x => Lean.Parser.symbol ":"))) fun x => Lean.Parser.termParser Lean.Parser.maxPrec)

source

def Lean.Parser.Term.defaultOrOfNonempty :

Lean.Parser.Parser

Equations

Lean.Parser.Term.defaultOrOfNonempty = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "defaultOrOfNonempty" (some `Lean.Parser.Term.defaultOrOfNonempty)) (Lean.Parser.leadingNode `Lean.Parser.Term.defaultOrOfNonempty 1024 (Lean.Parser.symbol "default_or_ofNonempty%"))

source

def Lean.Parser.Term.namedArgument :

Lean.Parser.Parser

Equations

Lean.Parser.Term.namedArgument = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "namedArgument" (some `Lean.Parser.Term.namedArgument)) (Lean.Parser.leadingNode `Lean.Parser.Term.namedArgument 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => Lean.Parser.symbol " := ")) fun x => HAndThen.hAndThen Lean.Parser.termParser fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.pipeProj :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.pipeProj = Lean.Parser.trailingNode `Lean.Parser.Term.pipeProj Lean.Parser.minPrec 0 (HAndThen.hAndThen (Lean.Parser.symbol " |>.") fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.fieldIdx fun x => Lean.Parser.Term.ident) fun x => Lean.Parser.many Lean.Parser.Term.argument)

source

def Lean.Parser.Term.ellipsis :

Lean.Parser.Parser

Equations

Lean.Parser.Term.ellipsis = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "ellipsis" (some `Lean.Parser.Term.ellipsis)) (Lean.Parser.leadingNode `Lean.Parser.Term.ellipsis 1024 (Lean.Parser.symbol ".."))

source

def Lean.Parser.Term.pipeCompletion :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.pipeCompletion = Lean.Parser.trailingNode `Lean.Parser.Term.pipeCompletion Lean.Parser.minPrec 0 (Lean.Parser.symbol " |>.")

source

def Lean.Parser.Term.argument :

Lean.Parser.Parser

Equations

Lean.Parser.Term.argument = HAndThen.hAndThen (Lean.Parser.checkWsBefore "expected space") fun x => HAndThen.hAndThen (Lean.Parser.checkColGt "expected to be indented") fun x => HOrElse.hOrElse Lean.Parser.Term.namedArgument fun x => HOrElse.hOrElse Lean.Parser.Term.ellipsis fun x => Lean.Parser.termParser Lean.Parser.argPrec

source

def Lean.Parser.Term.subst :

Lean.Parser.TrailingParser

Equations

Lean.Parser.Term.subst = Lean.Parser.trailingNode `Lean.Parser.Term.subst 75 0 (HAndThen.hAndThen (Lean.Parser.symbol " ▸ ") fun x => Lean.Parser.sepBy1 (Lean.Parser.termParser 75) " ▸ " (Lean.Parser.symbol " ▸ "))

source

def Lean.Parser.Term.funBinder.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.funBinder.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.funBinder.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.funBinder.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(funBinder|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth (Lean.Parser.evalInsideQuot `Lean.Parser.Term.funBinder Lean.Parser.Term.funBinder)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.bracketedBinder.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.bracketedBinder.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.bracketedBinder.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.bracketedBinder.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(bracketedBinder|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth (Lean.Parser.evalInsideQuot `Lean.Parser.Term.bracketedBinderF Lean.Parser.Term.bracketedBinder)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.matchDiscr.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.matchDiscr.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.matchDiscr.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.matchDiscr.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(matchDiscr|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth (Lean.Parser.evalInsideQuot `Lean.Parser.Term.matchDiscr Lean.Parser.Term.matchDiscr)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.attr.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.attr.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Term.attr.quot)) (Lean.Parser.leadingNode `Lean.Parser.Term.attr.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(attr|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth Lean.Parser.attrParser) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.panic :

Lean.Parser.Parser

Equations

Lean.Parser.Term.panic = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "panic" (some `Lean.Parser.Term.panic)) (Lean.Parser.leadingNode `Lean.Parser.Term.panic Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.symbol "panic! ") fun x => Lean.Parser.termParser))

source

def Lean.Parser.Term.unreachable :

Lean.Parser.Parser

Equations

Lean.Parser.Term.unreachable = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "unreachable" (some `Lean.Parser.Term.unreachable)) (Lean.Parser.leadingNode `Lean.Parser.Term.unreachable Lean.Parser.leadPrec (Lean.Parser.symbol "unreachable!"))

source

def Lean.Parser.Term.dbgTrace :

Lean.Parser.Parser

Equations

Lean.Parser.Term.dbgTrace = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "dbgTrace" (some `Lean.Parser.Term.dbgTrace)) (Lean.Parser.leadingNode `Lean.Parser.Term.dbgTrace Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "dbg_trace") fun x => HOrElse.hOrElse (Lean.Parser.interpolatedStr Lean.Parser.termParser) fun x => Lean.Parser.termParser)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.assert :

Lean.Parser.Parser

Equations

Lean.Parser.Term.assert = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "assert" (some `Lean.Parser.Term.assert)) (Lean.Parser.leadingNode `Lean.Parser.Term.assert Lean.Parser.leadPrec (HAndThen.hAndThen (Lean.Parser.withPosition (HAndThen.hAndThen (Lean.Parser.symbol "assert! ") fun x => Lean.Parser.termParser)) fun x => Lean.Parser.Term.optSemicolon Lean.Parser.termParser))

source

def Lean.Parser.Term.isIdent (stx : Lean.Syntax) :

Bool

Equations

Lean.Parser.Term.isIdent stx = (Lean.Syntax.isAntiquot stx || Lean.Syntax.isIdent stx)

source

def Lean.Parser.Term.stateRefT :

Lean.Parser.Parser

Equations

Lean.Parser.Term.stateRefT = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "stateRefT" (some `Lean.Parser.Term.stateRefT)) (Lean.Parser.leadingNode `Lean.Parser.Term.stateRefT 1024 (HAndThen.hAndThen (Lean.Parser.symbol "StateRefT") fun x => HAndThen.hAndThen Lean.Parser.Term.macroArg fun x => Lean.Parser.Term.macroLastArg))

source

def Lean.Parser.Term.dynamicQuot :

Lean.Parser.Parser

Equations

Lean.Parser.Term.dynamicQuot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "dynamicQuot" (some `Lean.Parser.Term.dynamicQuot)) (Lean.Parser.leadingNode `Lean.Parser.Term.dynamicQuot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(") fun x => HAndThen.hAndThen Lean.Parser.Term.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol "|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth (Lean.Parser.parserOfStack 1)) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Tactic.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Tactic.quot)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(tactic|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth Lean.Parser.tacticParser) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Tactic.quotSeq :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.quotSeq = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quotSeq" (some `Lean.Parser.Tactic.quotSeq)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.quotSeq 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(tactic|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth Lean.Parser.Tactic.seq1) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.bracketedBinderF :

Lean.Parser.Parser

Equations

Lean.Parser.Term.bracketedBinderF = Lean.Parser.Term.bracketedBinder

source

def Lean.Parser.Level.quot :

Lean.Parser.Parser

Equations

Lean.Parser.Level.quot = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "quot" (some `Lean.Parser.Level.quot)) (Lean.Parser.leadingNode `Lean.Parser.Level.quot 1024 (HAndThen.hAndThen (Lean.Parser.symbol "`(level|") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth Lean.Parser.levelParser) fun x => Lean.Parser.symbol ")"))

source

def Lean.Parser.Term.macroArg :

Lean.Parser.Parser

Equations

Lean.Parser.Term.macroArg = Lean.Parser.termParser Lean.Parser.maxPrec

source

def Lean.Parser.Term.macroDollarArg :

Lean.Parser.Parser

Equations

Lean.Parser.Term.macroDollarArg = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macroDollarArg" (some `Lean.Parser.Term.macroDollarArg)) (Lean.Parser.leadingNode `Lean.Parser.Term.macroDollarArg 1024 (HAndThen.hAndThen (Lean.Parser.symbol "$") fun x => Lean.Parser.termParser 10))

source

def Lean.Parser.Term.macroLastArg :

Lean.Parser.Parser

Equations

Lean.Parser.Term.macroLastArg = HOrElse.hOrElse Lean.Parser.Term.macroDollarArg fun x => Lean.Parser.Term.macroArg