# Documentation

Lean.Elab.Tactic.Conv.Basic

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

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.
Equations
• One or more equations did not get rendered due to their size.

Given lhs, runs the conv tactic with the goal ⊢ lhs = ?rhs⊢ 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.
Equations
• One or more equations did not get rendered due to their size.
Equations
Equations

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

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

Replace lhs with the definitionally equal lhs'.

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

Evaluate sepByIndent conv "; "

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

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

Equations
• One or more equations did not get rendered due to their size.
Equations
• = let seq := stx[2];
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.