def Lean.Elab.Tactic.Conv.mkLHSGoal (e : Expr) : MetaM 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 : Expr) (tag : Name := Name.anonymous) : MetaM (Expr × 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 : MVarId) : MetaM MVarId

def Lean.Elab.Tactic.Conv.convert (lhs : Expr) (conv : TacticM Unit) : TacticM (Expr × 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 : MVarId) : MetaM (Expr × Expr)

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

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

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

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

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

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

Replace lhs with the definitionally equal lhs'.

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

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

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

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

Evaluate `sepByIndent conv "; "

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

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

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

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

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

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

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

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

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

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

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

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

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