Getting type signature displayed

Stream: new members

[Daniel Fabian]

Is there a way in the vscode extension to get the type signature displayed other than #check?

[Bryan Gin-ge Chen]

You can hover over names in the middle of term proofs (and sometimes in tactic proofs) to see a popup with the type. If your text cursor is in the middle of such a name, there's a spot in the status bar that shows the type (sadly, it won't be displayed if it's too long).

If you want to look up the type of a declaration, you can hit Ctrl+T for the "symbol search". Then if you type in what you're interested in, you should see the type in the list of suggestions.

I think @Edward Ayers's infoview rework may also include widgets that allow one to inspect the types of terms in the tactic state / goal.

[Bryan Gin-ge Chen]

Another option (for term proofs) is to surround the code you're interested in with {! and !}, then select the "show term" code action from the "lightbulb" menu. See also this message which gives code for a keybinding that makes using hole commands easier.