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.

Equations

• Lean.Elab.Tactic.Conv.mkLHSGoal e = match e.eq? with | some val => pure (Lean.mkLHSGoalRaw e) | x => do let __do_lift ← Lean.Meta.whnf e pure (Lean.mkLHSGoalRaw __do_lift)

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.getLhsRhs = do let __do_lift ← Lean.Elab.Tactic.getMainGoal liftM (Lean.Elab.Tactic.Conv.getLhsRhsCore __do_lift)

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

Equations

• Lean.Elab.Tactic.Conv.getLhs = do let __do_lift ← Lean.Elab.Tactic.Conv.getLhsRhs pure __do_lift.fst

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

Equations

• Lean.Elab.Tactic.Conv.getRhs = do let __do_lift ← Lean.Elab.Tactic.Conv.getLhsRhs pure __do_lift.snd

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Replace lhs with the definitionally equal lhs'.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Tactic.Conv.evalClear : Tactic

Equations

• One or more equations did not get rendered due to their size.

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

Evaluate `sepByIndent conv "; "

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalConvSeq1Indented stx = Lean.Elab.Tactic.Conv.evalSepByIndentConv stx[0]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalNestedConv stx = Lean.Elab.Tactic.Conv.evalConvSeqBracketed stx[0]

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

Equations

• Lean.Elab.Tactic.Conv.evalConvSeq stx = Lean.Elab.Tactic.evalTactic stx[0]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalParen stx = Lean.Elab.Tactic.evalTactic stx[1]

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalNestedTacticCore stx = do Lean.Elab.Tactic.evalTactic stx[2] Lean.Elab.Tactic.Conv.remarkAsConvGoal

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalConvTactic stx = Lean.Elab.Tactic.evalTactic stx[2]

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Lean.Elab.Tactic.Conv.evalFirst = Lean.Elab.Tactic.evalFirst