Printing of LHS goals

Stream: lean4

[Leni Aniva]

In this example:

example : ∀ (a b c: Nat), (a + b) + c = (b + a) + c := by
  intro a b c
  conv =>
    lhs

when the cursor is on the conv => line, LSP displays the goal as

Goals (1)
a b c : Nat
| a + b + c = b + a + c

where the | on the left shows that this goal is a LHS goal. This is because the goal prefix in ppGoal is determined by it:

def getGoalPrefix (mvarDecl : MetavarDecl) : String :=
  if isLHSGoal? mvarDecl.type |>.isSome then
    -- use special prefix for `conv` goals
    "| "
  else
    "⊢ "

However, this is in contradiction to this comment in Lean/Expr.lean:

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

This version of `mkLHSGoal` does not check that the argument is an equality.
-/
def mkLHSGoalRaw (e : Expr) : Expr :=
  mkAnnotation `_lhsGoal e

If a goal is a LHS goal, then according to this comment it cannot be pretty printed as lhs = rhs but instead as lhs only. How does the conv tactic manage to print a goal as | lhs = rhs?

[Joachim Breitner]

There are two different LHSs that are easily confused:

If the goal is P, and you start

conv =>

then it creates a goal P = ?rhs with an unknown ?rhs (a mvar), and the isLHSGoal makes sure you don't see

⊢ P = ?rhs

but

| P

instead.

In your case, the P itself happens to be an equality (a + b) + c = (a + b) + c, and so you see that.