Stream: new members
Daniel Fabian (May 21 2020 at 00:10):
Is there a way in the vscode extension to get the type signature displayed other than
Bryan Gin-ge Chen (May 21 2020 at 00:23):
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 (May 21 2020 at 00:25):
Another option (for term proofs) is to surround the code you're interested in with
!}, 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.
Last updated: May 13 2021 at 21:12 UTC