InfoView

Some functionality of InfoView in the Lean 4 VS Code extension is covered by generic LSP features found in Vim 9. Lean-specific functionality beyond LSP can be found in Lean editor sidekick applications such as Plean Sidekick.

The location list window in Vim roughly corresponds to the messages list in InfoView. 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.