Term goal and local context query request s.p.e.p. (Pre-RFC)

Stream: lean4

[Gabriel Ebner]

Term goal and local context query request server protocol extension proposal (Pre-RFC)

Introduction

Tactic proofs are easy to follow because you can step through them line by line and watch how the tactic state changes. Lean 3.15 therefore extended this feature to term-mode proofs. With this change, Lean also shows for every subterm a tactic state, printing the local context and the expected type.

This feature makes it easy to understand term-mode proofs since you can now step through them just like a tactic proof. It is also useful when reading code, since it tells you the names and types of local variables.

Proposal

In analogy to the $/lean/plainGoal request, we add a $/lean/plainTermGoal request, returning a pretty-printed goal state consisting of the local context and the expected type at the given position.

interface PlainTermGoalParams extends TextDocumentPositionParams {}

interface PlainTermGoal {
  goal: string;
}

In the editor, the term goal state would be shown separately and below of the tactic state. (This is sometimes a bit confusing in Lean 3, when the term goal was shown instead of the tactic state.)

[Sebastian Ullrich]

I see, showing the term goal in addition to and after the tactic goal should address the concerns I had about this feature. For example, didn't test this in Lean 3, but we probably still want to look at the tactic goal when placing the cursor on rw [h hp]