Equations
- Lean.Parser.Tactic.Conv.conv.quot = Lean.ParserDescr.node `Lean.Parser.Term.quot 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "`(conv|") (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `incQuotDepth (Lean.ParserDescr.cat `conv 0)) (Lean.ParserDescr.symbol ")")))
Equations
- Lean.Parser.Tactic.Conv.convSeq1Indented = Lean.ParserDescr.nodeWithAntiquot "convSeq1Indented" `Lean.Parser.Tactic.Conv.convSeq1Indented (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.cat `conv 0)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol ";"))))))
Equations
- Lean.Parser.Tactic.Conv.convSeqBracketed = Lean.ParserDescr.nodeWithAntiquot "convSeqBracketed" `Lean.Parser.Tactic.Conv.convSeqBracketed (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "{") (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.cat `conv 0) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol ";")))))) (Lean.ParserDescr.symbol "}"))
Equations
- Lean.Parser.Tactic.Conv.convSeq = Lean.ParserDescr.nodeWithAntiquot "convSeq" `Lean.Parser.Tactic.Conv.convSeq (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.Conv.convSeq1Indented Lean.Parser.Tactic.Conv.convSeqBracketed)
Equations
- Lean.Parser.Tactic.Conv.conv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.conv 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "conv " false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " at ") (Lean.ParserDescr.const `ident)))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " in ") (Lean.ParserDescr.cat `term 0)))) (Lean.ParserDescr.symbol " => ")) Lean.Parser.Tactic.Conv.convSeq)
Equations
- Lean.Parser.Tactic.Conv.lhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.lhs 1024 (Lean.ParserDescr.nonReservedSymbol "lhs" false)
Equations
- Lean.Parser.Tactic.Conv.rhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rhs 1024 (Lean.ParserDescr.nonReservedSymbol "rhs" false)
Equations
- Lean.Parser.Tactic.Conv.whnf = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.whnf 1024 (Lean.ParserDescr.nonReservedSymbol "whnf" false)
Equations
- Lean.Parser.Tactic.Conv.reduce = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.reduce 1024 (Lean.ParserDescr.nonReservedSymbol "reduce" false)
Equations
- Lean.Parser.Tactic.Conv.congr = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.congr 1024 (Lean.ParserDescr.nonReservedSymbol "congr" false)
Equations
- Lean.Parser.Tactic.Conv.arg = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.arg 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "arg " false) (Lean.ParserDescr.const `num))
Equations
- Lean.Parser.Tactic.Conv.ext = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.ext 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "ext " false) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.const `ident))))
Equations
- Lean.Parser.Tactic.Conv.change = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.change 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "change " false) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.Conv.delta = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.delta 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "delta " false) (Lean.ParserDescr.const `ident))
Equations
- Lean.Parser.Tactic.Conv.unfold = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.unfold 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "unfold " false) (Lean.ParserDescr.const `ident))
Equations
- Lean.Parser.Tactic.Conv.pattern = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.pattern 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "pattern " false) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.Conv.rewrite = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rewrite 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rewrite " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) Lean.Parser.Tactic.rwRuleSeq)
Equations
- Lean.Parser.Tactic.Conv.simp = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.simp 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "simp " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.discharger)) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.nonReservedSymbol "only " false))) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "[") (Lean.ParserDescr.sepBy (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpStar (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.simpErase Lean.Parser.Tactic.simpLemma)) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]"))))
Equations
- Lean.Parser.Tactic.Conv.simpMatch = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.simpMatch 1024 (Lean.ParserDescr.nonReservedSymbol "simp_match " false)
Equations
- Lean.Parser.Tactic.Conv.nestedTacticCore = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedTacticCore 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "tactic'" false) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.Conv.nestedTactic = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedTactic 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "tactic" false) (Lean.ParserDescr.symbol " => ")) (Lean.ParserDescr.const `tacticSeq))
Equations
- Lean.Parser.Tactic.Conv.nestedConv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedConv 1022 Lean.Parser.Tactic.Conv.convSeqBracketed
Equations
- Lean.Parser.Tactic.Conv.paren = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.paren 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "(" false) Lean.Parser.Tactic.Conv.convSeq) (Lean.ParserDescr.symbol ")"))
Equations
- Lean.Parser.Tactic.Conv.convConvSeq = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convConvSeq 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "conv " false) (Lean.ParserDescr.symbol " => ")) Lean.Parser.Tactic.Conv.convSeq)
Equations
- Lean.Parser.Tactic.Conv.«conv·._» = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.«conv·._» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.symbol "·") (Lean.ParserDescr.symbol ".")) Lean.Parser.Tactic.Conv.convSeq)
Equations
- Lean.Parser.Tactic.Conv.convRw__ = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRw__ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "rw " false) (Lean.ParserDescr.unary `optional Lean.Parser.Tactic.config)) Lean.Parser.Tactic.rwRuleSeq)
Equations
- Lean.Parser.Tactic.Conv.convErw_ = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convErw_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "erw " false) Lean.Parser.Tactic.rwRuleSeq)
Equations
- Lean.Parser.Tactic.Conv.convArgs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convArgs 1024 (Lean.ParserDescr.nonReservedSymbol "args" false)
Equations
- Lean.Parser.Tactic.Conv.convLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)
Equations
- Lean.Parser.Tactic.Conv.convRight = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRight 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)
Equations
- Lean.Parser.Tactic.Conv.convIntro___ = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convIntro___ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "intro " false) (Lean.ParserDescr.unary `many (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) (Lean.ParserDescr.const `ident))))
Equations
- Lean.Parser.Tactic.Conv.enterArg = Lean.ParserDescr.nodeWithAntiquot "enterArg" `Lean.Parser.Tactic.Conv.enterArg (Lean.ParserDescr.binary `orelse (Lean.ParserDescr.const `ident) (Lean.ParserDescr.const `num))
Equations
- Lean.Parser.Tactic.Conv.«convEnter[__]» = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.«convEnter[__]» 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "enter " false) (Lean.ParserDescr.symbol "[")) (Lean.ParserDescr.sepBy1 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGt) Lean.Parser.Tactic.Conv.enterArg) "," (Lean.ParserDescr.symbol ", "))) (Lean.ParserDescr.symbol "]"))
Equations
- Lean.Parser.Tactic.Conv.convSkip = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convSkip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)
Equations
- Lean.Parser.Tactic.Conv.convDone = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convDone 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)
Equations
- Lean.Parser.Tactic.Conv.convTrace_state = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convTrace_state 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)
Equations
- Lean.Parser.Tactic.Conv.convApply_ = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convApply_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "apply " false) (Lean.ParserDescr.cat `term 0))
Equations
- Lean.Parser.Tactic.Conv.first = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.first 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "first " false) (Lean.ParserDescr.unary `withPosition (Lean.ParserDescr.unary `many1 (Lean.ParserDescr.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.const `colGe) (Lean.ParserDescr.symbol "|")) Lean.Parser.Tactic.Conv.convSeq)))))
Equations
- Lean.Parser.Tactic.Conv.convRepeat_ = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRepeat_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "repeat " false) Lean.Parser.Tactic.Conv.convSeq)