source
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)

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

source
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)

Instances For

source
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

Instances For

source
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

Instances For

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

Instances For

source
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

Instances For

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

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

Instances For

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

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

Instances For

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

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

Instances For

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

- Lean.Elab.Tactic.Conv.evalFirst = Lean.Elab.Tactic.evalFirst

Instances For