def Lean.Elab.Tactic.Conv.mkLHSGoal (e : Lean.Expr) : Lean.MetaM Lean.Expr

Annotate e with the LHS annotation. The delaborator displays expressions of the form lhs = rhs as lhs when they have this annotation. This is used to implement the infoview for the conv mode.

def Lean.Elab.Tactic.Conv.mkConvGoalFor (lhs : Lean.Expr) (tag : optParam Lake.Name Lean.Name.anonymous) : Lean.MetaM (Lean.Expr × Lean.Expr)

Given lhs, returns a pair of metavariables (?rhs, ?newGoal) where ?newGoal : lhs = ?rhs. tag is the name of newGoal.

def Lean.Elab.Tactic.Conv.markAsConvGoal (mvarId : Lean.MVarId) : Lean.MetaM Lean.MVarId

def Lean.Elab.Tactic.Conv.convert (lhs : Lean.Expr) (conv : Lean.Elab.Tactic.TacticM Unit) : Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)

Given lhs, runs the conv tactic with the goal ⊢ lhs = ?rhs. conv should produce no remaining goals that are not solvable with refl. Returns a pair of instantiated expressions (?rhs, ?p) where ?p : lhs = ?rhs.

def Lean.Elab.Tactic.Conv.getLhsRhsCore (mvarId : Lean.MVarId) : Lean.MetaM (Lean.Expr × Lean.Expr)

def Lean.Elab.Tactic.Conv.getLhsRhs : Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)

def Lean.Elab.Tactic.Conv.getLhs : Lean.Elab.Tactic.TacticM Lean.Expr

def Lean.Elab.Tactic.Conv.getRhs : Lean.Elab.Tactic.TacticM Lean.Expr

def Lean.Elab.Tactic.Conv.updateLhs (lhs' : Lean.Expr) (h : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

⊢ lhs = rhs ~~> ⊢ lhs' = rhs using h : lhs = lhs'.

def Lean.Elab.Tactic.Conv.changeLhs (lhs' : Lean.Expr) : Lean.Elab.Tactic.TacticM Unit

Replace lhs with the definitionally equal lhs'.

def Lean.Elab.Tactic.Conv.evalWhnf : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalReduce : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalZeta : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalSepByIndentConv (stx : Lean.Syntax) : Lean.Elab.Tactic.TacticM Unit

Evaluate `sepByIndent conv "; "

def Lean.Elab.Tactic.Conv.evalConvSeq1Indented : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalConvSeqBracketed : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalNestedConv : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalConvSeq : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalConvConvSeq : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalParen : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.remarkAsConvGoal : Lean.Elab.Tactic.TacticM Unit

Mark goals of the form ⊢ a = ?m .. with the conv goal annotation

def Lean.Elab.Tactic.Conv.evalNestedTacticCore : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalNestedTactic : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalConvTactic : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalConv : Lean.Elab.Tactic.Tactic

def Lean.Elab.Tactic.Conv.evalFirst : Lean.Elab.Tactic.Tactic