Documentation

Lean.Parser.Tactic

def Lean.Parser.Tactic.unknown :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.unknown = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "unknown" (some `Lean.Parser.Tactic.unknown)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.unknown 1024 (Lean.Parser.withPosition (HAndThen.hAndThen Lean.Parser.ident fun x => Lean.Parser.errorAtSavedPos "unknown tactic" true)))

def Lean.Parser.Tactic.nestedTactic :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.nestedTactic = Lean.Parser.Tactic.tacticSeqBracketed

def Lean.Parser.Tactic.eraseAuxDiscrs :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.eraseAuxDiscrs = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "eraseAuxDiscrs" (some `Lean.Parser.Tactic.eraseAuxDiscrs)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.eraseAuxDiscrs Lean.Parser.maxPrec (Lean.Parser.symbol "eraseAuxDiscrs!"))

def Lean.Parser.Tactic.matchRhs :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.matchRhs = HOrElse.hOrElse Lean.Parser.Term.hole fun x => HOrElse.hOrElse Lean.Parser.Term.syntheticHole fun x => Lean.Parser.Tactic.tacticSeq

def Lean.Parser.Tactic.matchAlts :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.matchAlts = Lean.Parser.Term.matchAlts Lean.Parser.Tactic.matchRhs

def Lean.Parser.Tactic.match :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.match = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "match" (some `Lean.Parser.Tactic.match)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.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.Tactic.matchAlts))

def Lean.Parser.Tactic.introMatch :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.introMatch = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "introMatch" (some `Lean.Parser.Tactic.introMatch)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.introMatch 1024 (HAndThen.hAndThen (Lean.Parser.nonReservedSymbol "intro ") fun x => Lean.Parser.Tactic.matchAlts))

def Lean.Parser.Tactic.decide :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.decide = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "decide" (some `Lean.Parser.Tactic.decide)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.decide 1024 (Lean.Parser.nonReservedSymbol "decide"))

def Lean.Parser.Tactic.nativeDecide :

Lean.Parser.Parser

Equations

Lean.Parser.Tactic.nativeDecide = Lean.Parser.withAntiquot (Lean.Parser.mkAntiquot "nativeDecide" (some `Lean.Parser.Tactic.nativeDecide)) (Lean.Parser.leadingNode `Lean.Parser.Tactic.nativeDecide 1024 (Lean.Parser.nonReservedSymbol "nativeDecide"))