Zulip Chat Archive

Stream: new members

Topic: Getting type signature displayed


view this post on Zulip Daniel Fabian (May 21 2020 at 00:10):

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

view this post on Zulip 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.

view this post on Zulip 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 {! 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.


Last updated: May 13 2021 at 21:12 UTC