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.

Equations

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

def Lean.Elab.Tactic.Conv.mkConvGoalFor (lhs : Lean.Expr) (tag : optParam Lean.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.

Equations

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

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

Equations

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

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.

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Lean.Elab.Tactic.Conv.changeLhs (lhs' : Lean.Expr) : Lean.Elab.Tactic.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 : Lean.Elab.Tactic.Tactic

Equations

• Lean.Elab.Tactic.Conv.evalWhnf x = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let a ← liftM (Lean.Meta.whnf a) Lean.Elab.Tactic.Conv.changeLhs a

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Conv.evalZeta x = Lean.Elab.Tactic.withMainContext do let a ← Lean.Elab.Tactic.Conv.getLhs let a ← liftM (Lean.Meta.zetaReduce a) Lean.Elab.Tactic.Conv.changeLhs a

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

Evaluate `sepByIndent conv "; "

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

• Lean.Elab.Tactic.Conv.evalNestedTacticCore stx = let seq := stx[2]; do Lean.Elab.Tactic.evalTactic seq Lean.Elab.Tactic.Conv.remarkAsConvGoal

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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