InfoView

The location list window in Vim roughly corresponds to the InfoView feature of the Lean 4 VS Code extension.

Using the Vim :lopen (or :lop) command will open the location list window, which contains diagnostic messages generated by Lean. These diagnostic messages from Lean contain some of the information found in InfoView, but in a much less user-friendly format, as you'd expect in Vim.

For more details, see Vim :help location-list and :help lsp.txt.

Tips & Tricks

If you want a diagnostic message that indicates whether a theorem somethingIsStuff is proven, you can add the following line:

#print axioms somethingIsStuff

If the theorem does not depend on the axiom sorryAx, then the proof goal has been accomplished. For example:

theorem vimGreaterThanEmacs: True := trivial
#print axioms vimGreaterThanEmacs

generates the diagnostic message:

truth.lean|2 col 1-7 info| 'vimGreaterThanEmacs' does not depend on any axioms

so we can see the statement is true, obviously.