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