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.convClear (mvarId : MVarId) (fvarId : FVarId) : MetaM MVarId

Removes the hypothesis referred to by fvarId from the context of the currently focused conv goal, provided that fvarId is not referenced by another hypothesis or the current conv-focused target.

def Lean.Elab.Tactic.Conv.evalClear : 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