Show term goals.

[gebner]

Companion PR to leanprover/lean4#504. There should be no merge conflicts with #35.

[Julian]

Very cool.

One functional question -- I tried your first test case from leanprover/lean4#518:

example : 0 < 2 :=
  Nat.ltTrans Nat.zeroLtOne (Nat.ltSuccSelf _)
                         --^ $/lean/plainTermGoal

and if I put the cursor in the above spot rather than one of the ones in the test case, what I see in the infoview is:

▶ expected type (2:3-2:47)
⊢ 0 < 2

i.e. the expected type for the whole expression, whereas one character later I see:

▶ expected type (2:29-2:47)
⊢ 1 < 2

Without having any idea how much complexity it adds, wouldn't it be better to show the latter even in the space between, or is this way necessary for some reason?

And thanks again this looks super cool, feel free to merge presumably as soon as Leo merges the upstream PR or whatever.

[gebner]

Right, if you have f a b and put the cursor between a and b, then it shows the goal for f a b. It only shows goals for terms that intersect the cursor position. I'm not sure there's one single correct answer here. Apparently you've expected the goal for b, but the goal for a would make just as much sense.

That's why I've added a range to the response, so that it's at least clear what subterm the server picked. In another branch I have some code that highlights the range when you move your cursor over the "expected type" heading in the infoview: https://github.com/gebner/lean.nvim/tree/termgoal

Without having any idea how much complexity it adds,

There is a helper function that allows you to get the smallest info node (i.e. smallest covering range satisfying some predicate). I tried to keep the logic simple. It was already awkward enough to exclude the f in f a b (so that you get the goal for f a b instead of f's function type).

[Julian]

Aha. That makes a lot of sense, and for some reason I indeed did have the opposite expectation in the test case that did m < n (that I'd see the whole term) so I can see things getting funky there. Thanks for explaining (and yeah lgtm again).