Init.Conv

source

def Lean.Parser.Tactic.Conv.conv.quot :

Lean.ParserDescr

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.cat `conv 0) (Lean.ParserDescr.symbol ")")))

source

def Lean.Parser.Tactic.Conv.convSeq1Indented :

Lean.ParserDescr

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 ";"))))))

source

def Lean.Parser.Tactic.Conv.convSeqBracketed :

Lean.ParserDescr

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 "}"))

source

def Lean.Parser.Tactic.Conv.convSeq :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convSeq = Lean.ParserDescr.nodeWithAntiquot "convSeq" `Lean.Parser.Tactic.Conv.convSeq (Lean.ParserDescr.binary `orelse Lean.Parser.Tactic.Conv.convSeqBracketed Lean.Parser.Tactic.Conv.convSeq1Indented)

source

def Lean.Parser.Tactic.Conv.conv :

Lean.ParserDescr

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)

source

def Lean.Parser.Tactic.Conv.lhs :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.lhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.lhs 1024 (Lean.ParserDescr.nonReservedSymbol "lhs" false)

source

def Lean.Parser.Tactic.Conv.rhs :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.rhs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.rhs 1024 (Lean.ParserDescr.nonReservedSymbol "rhs" false)

source

def Lean.Parser.Tactic.Conv.whnf :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.whnf = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.whnf 1024 (Lean.ParserDescr.nonReservedSymbol "whnf" false)

source

def Lean.Parser.Tactic.Conv.reduce :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.reduce = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.reduce 1024 (Lean.ParserDescr.nonReservedSymbol "reduce" false)

Put term in normal form, this tactic is ment for debugging purposes only

source

def Lean.Parser.Tactic.Conv.congr :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.congr = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.congr 1024 (Lean.ParserDescr.nonReservedSymbol "congr" false)

source

def Lean.Parser.Tactic.Conv.arg :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.arg = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.arg 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "arg " false) (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol "@"))) (Lean.ParserDescr.const `num))

source

def Lean.Parser.Tactic.Conv.ext :

Lean.ParserDescr

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))))

source

def Lean.Parser.Tactic.Conv.change :

Lean.ParserDescr

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))

source

def Lean.Parser.Tactic.Conv.delta :

Lean.ParserDescr

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))

source

def Lean.Parser.Tactic.Conv.unfold :

Lean.ParserDescr

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))

source

def Lean.Parser.Tactic.Conv.pattern :

Lean.ParserDescr

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))

source

def Lean.Parser.Tactic.Conv.rewrite :

Lean.ParserDescr

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)

source

def Lean.Parser.Tactic.Conv.simp :

Lean.ParserDescr

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 "]"))))

source

def Lean.Parser.Tactic.Conv.simpMatch :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.simpMatch = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.simpMatch 1024 (Lean.ParserDescr.nonReservedSymbol "simp_match " false)

source

def Lean.Parser.Tactic.Conv.nestedTacticCore :

Lean.ParserDescr

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))

Execute the given tactic block without converting conv goal into a regular goal

source

def Lean.Parser.Tactic.Conv.nestedTactic :

Lean.ParserDescr

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))

Focus, convert the conv goal ⊢lhs into a regular goal ⊢lhs=rhs, and then execute the given tactic block.

source

def Lean.Parser.Tactic.Conv.nestedConv :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.nestedConv = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.nestedConv 1022 Lean.Parser.Tactic.Conv.convSeqBracketed

source

def Lean.Parser.Tactic.Conv.paren :

Lean.ParserDescr

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 ")"))

source

def Lean.Parser.Tactic.Conv.convConvSeq :

Lean.ParserDescr

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)

source

def Lean.Parser.Tactic.Conv.«conv·._» :

Lean.ParserDescr

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)

·conv focuses on the main conv goal and tries to solve it using s

source

def Lean.Parser.Tactic.Conv.convRw__ :

Lean.ParserDescr

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)

source

def Lean.Parser.Tactic.Conv.convErw_ :

Lean.ParserDescr

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)

source

def Lean.Parser.Tactic.Conv.convArgs :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convArgs = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convArgs 1024 (Lean.ParserDescr.nonReservedSymbol "args" false)

source

def Lean.Parser.Tactic.Conv.convLeft :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convLeft = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convLeft 1024 (Lean.ParserDescr.nonReservedSymbol "left" false)

source

def Lean.Parser.Tactic.Conv.convRight :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convRight = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convRight 1024 (Lean.ParserDescr.nonReservedSymbol "right" false)

source

def Lean.Parser.Tactic.Conv.convIntro___ :

Lean.ParserDescr

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))))

source

def Lean.Parser.Tactic.Conv.enterArg :

Lean.ParserDescr

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.unary `group (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.unary `optional (Lean.ParserDescr.symbol "@")) (Lean.ParserDescr.const `num))))

source

def Lean.Parser.Tactic.Conv.«convEnter[__]» :

Lean.ParserDescr

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 "]"))

source

def Lean.Parser.Tactic.Conv.convSkip :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convSkip = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convSkip 1024 (Lean.ParserDescr.nonReservedSymbol "skip" false)

source

def Lean.Parser.Tactic.Conv.convDone :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convDone = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convDone 1024 (Lean.ParserDescr.nonReservedSymbol "done" false)

source

def Lean.Parser.Tactic.Conv.convTrace_state :

Lean.ParserDescr

Equations

Lean.Parser.Tactic.Conv.convTrace_state = Lean.ParserDescr.node `Lean.Parser.Tactic.Conv.convTrace_state 1024 (Lean.ParserDescr.nonReservedSymbol "trace_state" false)

source

def Lean.Parser.Tactic.Conv.convApply_ :

Lean.ParserDescr

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))

source

def Lean.Parser.Tactic.Conv.first :

Lean.ParserDescr

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)))))

first|conv|... runs each conv until one succeeds, or else fails.

source

def Lean.Parser.Tactic.Conv.convRepeat_ :

Lean.ParserDescr

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)