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.
Instances For
def
Lean.Elab.Tactic.Conv.mkConvGoalFor
(lhs : Lean.Expr)
(tag : optParam Lake.Name Lean.Name.anonymous)
:
Given lhs, returns a pair of metavariables (?rhs, ?newGoal)
where ?newGoal : lhs = ?rhs. tag is the name of newGoal.
Instances For
Instances For
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.
Instances For
Instances For
Instances For
⊢ lhs = rhs ~~> ⊢ lhs' = rhs using h : lhs = lhs'.
Instances For
Replace lhs with the definitionally equal lhs'.
Instances For
Evaluate `sepByIndent conv "; "
Instances For
Mark goals of the form ⊢ a = ?m .. with the conv goal annotation