Documentation

Lean.Parser.Syntax

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.precedenceParser rbp = Lean.Parser.categoryParser `prec rbp

@[inline]

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

Lean.Parser.Parser

Equations

Lean.Parser.syntaxParser rbp = Lean.Parser.categoryParser `stx rbp

def Lean.Parser.precedence :

Lean.Parser.Parser

Equations

Lean.Parser.precedence = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "precedence" (some `Lean.Parser.precedence)) (Lean.Parser.leadingNode `Lean.Parser.precedence 1024 (HAndThen.hAndThen (Lean.Parser.symbol ":") fun x => Lean.Parser.precedenceParser Lean.Parser.maxPrec))

def Lean.Parser.optPrecedence :

Lean.Parser.Parser

Equations

Lean.Parser.optPrecedence = Lean.Parser.optional (Lean.Parser.atomic Lean.Parser.precedence)

def Lean.Parser.Syntax.numPrec :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.numPrec = HAndThen.hAndThen (Lean.Parser.checkPrec Lean.Parser.maxPrec) fun x => Lean.Parser.numLit

def Lean.Parser.Syntax.paren :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.paren = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "paren" (some `Lean.Parser.Syntax.paren)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.paren 1024 (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Syntax.cat :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.cat = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "cat" (some `Lean.Parser.Syntax.cat)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.cat 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optPrecedence))

def Lean.Parser.Syntax.unary :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.unary = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "unary" (some `Lean.Parser.Syntax.unary)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.unary 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Syntax.binary :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.binary = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "binary" (some `Lean.Parser.Syntax.binary)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.binary 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen Lean.Parser.checkNoWsBefore fun x => HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Syntax.sepBy :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.sepBy = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "sepBy" (some `Lean.Parser.Syntax.sepBy)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.sepBy 1024 (HAndThen.hAndThen (Lean.Parser.symbol "sepBy(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => HAndThen.hAndThen Lean.Parser.strLit fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.many1 Lean.Parser.syntaxParser)) fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.nonReservedSymbol "allowTrailingSep")) fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Syntax.sepBy1 :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.sepBy1 = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "sepBy1" (some `Lean.Parser.Syntax.sepBy1)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.sepBy1 1024 (HAndThen.hAndThen (Lean.Parser.symbol "sepBy1(") fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.syntaxParser) fun x => HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => HAndThen.hAndThen Lean.Parser.strLit fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.many1 Lean.Parser.syntaxParser)) fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol ", ") fun x => Lean.Parser.nonReservedSymbol "allowTrailingSep")) fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Syntax.atom :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.atom = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "atom" (some `Lean.Parser.Syntax.atom)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.atom 1024 Lean.Parser.strLit)

def Lean.Parser.Syntax.nonReserved :

Lean.Parser.Parser

Equations

Lean.Parser.Syntax.nonReserved = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "nonReserved" (some `Lean.Parser.Syntax.nonReserved)) (Lean.Parser.leadingNode `Lean.Parser.Syntax.nonReserved 1024 (HAndThen.hAndThen (Lean.Parser.symbol "&") fun x => Lean.Parser.strLit))

def Lean.Parser.Term.stx.quot :

Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.prec.quot :

Lean.Parser.Parser

Equations

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

def Lean.Parser.Term.prio.quot :

Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.namedName :

Lean.Parser.Parser

Equations

Lean.Parser.Command.namedName = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "namedName" (some `Lean.Parser.Command.namedName)) (Lean.Parser.leadingNode `Lean.Parser.Command.namedName 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => Lean.Parser.nonReservedSymbol "name")) fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol ")"))

def Lean.Parser.Command.optNamedName :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optNamedName = Lean.Parser.optional Lean.Parser.Command.namedName

def Lean.Parser.Command.prefix :

Lean.Parser.Parser

Equations

Lean.Parser.Command.prefix = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "prefix" (some `Lean.Parser.Command.prefix)) (Lean.Parser.leadingNode `Lean.Parser.Command.prefix 1024 (Lean.Parser.symbol "prefix"))

def Lean.Parser.Command.infix :

Lean.Parser.Parser

Equations

Lean.Parser.Command.infix = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "infix" (some `Lean.Parser.Command.infix)) (Lean.Parser.leadingNode `Lean.Parser.Command.infix 1024 (Lean.Parser.symbol "infix"))

def Lean.Parser.Command.infixl :

Lean.Parser.Parser

Equations

Lean.Parser.Command.infixl = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "infixl" (some `Lean.Parser.Command.infixl)) (Lean.Parser.leadingNode `Lean.Parser.Command.infixl 1024 (Lean.Parser.symbol "infixl"))

def Lean.Parser.Command.infixr :

Lean.Parser.Parser

Equations

Lean.Parser.Command.infixr = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "infixr" (some `Lean.Parser.Command.infixr)) (Lean.Parser.leadingNode `Lean.Parser.Command.infixr 1024 (Lean.Parser.symbol "infixr"))

def Lean.Parser.Command.postfix :

Lean.Parser.Parser

Equations

Lean.Parser.Command.postfix = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "postfix" (some `Lean.Parser.Command.postfix)) (Lean.Parser.leadingNode `Lean.Parser.Command.postfix 1024 (Lean.Parser.symbol "postfix"))

def Lean.Parser.Command.mixfixKind :

Lean.Parser.Parser

Equations

Lean.Parser.Command.mixfixKind = HOrElse.hOrElse Lean.Parser.Command.prefix fun x => HOrElse.hOrElse Lean.Parser.Command.infix fun x => HOrElse.hOrElse Lean.Parser.Command.infixl fun x => HOrElse.hOrElse Lean.Parser.Command.infixr fun x => Lean.Parser.Command.postfix

def Lean.Parser.Command.mixfix :

Lean.Parser.Parser

Equations

Lean.Parser.Command.mixfix = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "mixfix" (some `Lean.Parser.Command.mixfix)) (Lean.Parser.leadingNode `Lean.Parser.Command.mixfix 1024 (HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen Lean.Parser.Command.mixfixKind fun x => HAndThen.hAndThen Lean.Parser.precedence fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedName fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen Lean.Parser.ppSpace fun x => HAndThen.hAndThen Lean.Parser.strLit fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.termParser))

def Lean.Parser.Command.identPrec :

Lean.Parser.Parser

Equations

Lean.Parser.Command.identPrec = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "identPrec" (some `Lean.Parser.Command.identPrec)) (Lean.Parser.leadingNode `Lean.Parser.Command.identPrec 1024 (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optPrecedence))

def Lean.Parser.Command.optKind :

Lean.Parser.Parser

Equations

Lean.Parser.Command.optKind = Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "kind") fun x => HAndThen.hAndThen (Lean.Parser.symbol ":=") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.symbol ")")

def Lean.Parser.Command.notationItem :

Lean.Parser.Parser

Equations

Lean.Parser.Command.notationItem = HAndThen.hAndThen Lean.Parser.ppSpace fun x => Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "notationItem" (some `Lean.Parser.Command.notationItem)) (HOrElse.hOrElse Lean.Parser.strLit fun x => Lean.Parser.Command.identPrec)

def Lean.Parser.Command.notation :

Lean.Parser.Parser

Equations

Lean.Parser.Command.notation = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "notation" (some `Lean.Parser.Command.notation)) (Lean.Parser.leadingNode `Lean.Parser.Command.notation 1024 (HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "notation") fun x => HAndThen.hAndThen Lean.Parser.optPrecedence fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedName fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen (Lean.Parser.many Lean.Parser.Command.notationItem) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.termParser))

def Lean.Parser.Command.macro_rules :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macro_rules = Lean.Parser.suppressInsideQuot (Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macro_rules" (some `Lean.Parser.Command.macro_rules)) (Lean.Parser.leadingNode `Lean.Parser.Command.macro_rules 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "macro_rules") fun x => HAndThen.hAndThen Lean.Parser.Command.optKind fun x => Lean.Parser.Term.matchAlts)))

def Lean.Parser.Command.syntax :

Lean.Parser.Parser

Equations

Lean.Parser.Command.syntax = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "syntax" (some `Lean.Parser.Command.syntax)) (Lean.Parser.leadingNode `Lean.Parser.Command.syntax 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "syntax ") fun x => HAndThen.hAndThen Lean.Parser.optPrecedence fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedName fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen (Lean.Parser.many1 (Lean.Parser.syntaxParser Lean.Parser.argPrec)) fun x => HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.ident))

def Lean.Parser.Command.syntaxAbbrev :

Lean.Parser.Parser

Equations

Lean.Parser.Command.syntaxAbbrev = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "syntaxAbbrev" (some `Lean.Parser.Command.syntaxAbbrev)) (Lean.Parser.leadingNode `Lean.Parser.Command.syntaxAbbrev 1024 (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen (Lean.Parser.symbol "syntax ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => Lean.Parser.many1 Lean.Parser.syntaxParser))

def Lean.Parser.Command.catBehaviorBoth :

Lean.Parser.Parser

Equations

Lean.Parser.Command.catBehaviorBoth = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "catBehaviorBoth" (some `Lean.Parser.Command.catBehaviorBoth)) (Lean.Parser.leadingNode `Lean.Parser.Command.catBehaviorBoth 1024 (Lean.Parser.nonReservedSymbol "both"))

def Lean.Parser.Command.catBehaviorSymbol :

Lean.Parser.Parser

Equations

Lean.Parser.Command.catBehaviorSymbol = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "catBehaviorSymbol" (some `Lean.Parser.Command.catBehaviorSymbol)) (Lean.Parser.leadingNode `Lean.Parser.Command.catBehaviorSymbol 1024 (Lean.Parser.nonReservedSymbol "symbol"))

def Lean.Parser.Command.catBehavior :

Lean.Parser.Parser

Equations

Lean.Parser.Command.catBehavior = Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol "(") fun x => HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "behavior") fun x => HAndThen.hAndThen (Lean.Parser.symbol " := ") fun x => HAndThen.hAndThen (HOrElse.hOrElse Lean.Parser.Command.catBehaviorBoth fun x => Lean.Parser.Command.catBehaviorSymbol) fun x => Lean.Parser.symbol ")")

def Lean.Parser.Command.syntaxCat :

Lean.Parser.Parser

Equations

Lean.Parser.Command.syntaxCat = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "syntaxCat" (some `Lean.Parser.Command.syntaxCat)) (Lean.Parser.leadingNode `Lean.Parser.Command.syntaxCat 1024 (HAndThen.hAndThen (Lean.Parser.symbol "declare_syntax_cat ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.Command.catBehavior))

def Lean.Parser.Command.macroArg :

Lean.Parser.Parser

Equations

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

def Lean.Parser.Command.macroRhs (quotP : Lean.Parser.Parser) :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macroRhs quotP = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macroRhs" (some `Lean.Parser.Command.macroRhs)) (Lean.Parser.leadingNode `Lean.Parser.Command.macroRhs 1024 (HOrElse.hOrElse (HAndThen.hAndThen (Lean.Parser.symbol "`(") fun x => HAndThen.hAndThen (Lean.Parser.incQuotDepth quotP) fun x => Lean.Parser.symbol ")") fun x => Lean.Parser.withPosition Lean.Parser.termParser))

def Lean.Parser.Command.macroTailTactic :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macroTailTactic = HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.identEq (Lean.Name.mkSimple "tactic"))) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.Command.macroRhs Lean.Parser.Tactic.seq1

def Lean.Parser.Command.macroTailCommand :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macroTailCommand = HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.identEq (Lean.Name.mkSimple "command"))) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.Command.macroRhs (Lean.Parser.many1Unbox Lean.Parser.commandParser)

def Lean.Parser.Command.macroTailDefault :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macroTailDefault = HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.ident)) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.Command.macroRhs (Lean.Parser.categoryParserOfStack 2)

def Lean.Parser.Command.macroTail :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macroTail = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macroTail" (some `Lean.Parser.Command.macroTail)) (Lean.Parser.leadingNode `Lean.Parser.Command.macroTail 1024 (HOrElse.hOrElse Lean.Parser.Command.macroTailTactic fun x => HOrElse.hOrElse Lean.Parser.Command.macroTailCommand fun x => Lean.Parser.Command.macroTailDefault))

def Lean.Parser.Command.macro :

Lean.Parser.Parser

Equations

Lean.Parser.Command.macro = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "macro" (some `Lean.Parser.Command.macro)) (Lean.Parser.leadingNode `Lean.Parser.Command.macro 1024 (Lean.Parser.suppressInsideQuot (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "macro ") fun x => HAndThen.hAndThen Lean.Parser.optPrecedence fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedName fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Command.macroArg) fun x => Lean.Parser.Command.macroTail)))

def Lean.Parser.Command.elab_rules :

Lean.Parser.Parser

Equations

Lean.Parser.Command.elab_rules = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "elab_rules" (some `Lean.Parser.Command.elab_rules)) (Lean.Parser.leadingNode `Lean.Parser.Command.elab_rules 1024 (Lean.Parser.suppressInsideQuot (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "elab_rules") fun x => HAndThen.hAndThen Lean.Parser.Command.optKind fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => Lean.Parser.ident)) fun x => HAndThen.hAndThen (Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " <= ") fun x => Lean.Parser.ident)) fun x => Lean.Parser.Term.matchAlts)))

def Lean.Parser.Command.elabArg :

Lean.Parser.Parser

Equations

Lean.Parser.Command.elabArg = Lean.Parser.Command.macroArg

def Lean.Parser.Command.elabTail :

Lean.Parser.Parser

Equations

Lean.Parser.Command.elabTail = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "elabTail" (some `Lean.Parser.Command.elabTail)) (Lean.Parser.leadingNode `Lean.Parser.Command.elabTail 1024 (HAndThen.hAndThen (Lean.Parser.atomic (HAndThen.hAndThen (Lean.Parser.symbol " : ") fun x => HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.optional (HAndThen.hAndThen (Lean.Parser.symbol " <= ") fun x => Lean.Parser.ident))) fun x => HAndThen.hAndThen Lean.Parser.darrow fun x => Lean.Parser.withPosition Lean.Parser.termParser))

def Lean.Parser.Command.elab :

Lean.Parser.Parser

Equations

Lean.Parser.Command.elab = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "elab" (some `Lean.Parser.Command.elab)) (Lean.Parser.leadingNode `Lean.Parser.Command.elab 1024 (Lean.Parser.suppressInsideQuot (HAndThen.hAndThen (Lean.Parser.optional Lean.Parser.Command.docComment) fun x => HAndThen.hAndThen Lean.Parser.Term.attrKind fun x => HAndThen.hAndThen (Lean.Parser.symbol "elab ") fun x => HAndThen.hAndThen Lean.Parser.optPrecedence fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedName fun x => HAndThen.hAndThen Lean.Parser.Command.optNamedPrio fun x => HAndThen.hAndThen (Lean.Parser.many1 Lean.Parser.Command.elabArg) fun x => Lean.Parser.Command.elabTail)))