List of available theorems

Stream: new members

[Patrick Johnson]

Is there a way in VS Code to get the list of available theorems in the autocomplete box? For example, I was searching for append_assoc from list, but it's not present in the autocomplete box, though It appears if I type append_as

Screenshot

[Kevin Buzzard]

Try the escape key and then ctrl-space again. This sometimes works. But I've never been able to figure this out. Sometimes stuff just doesn't get displayed and I don't know why.

[JJ]

Hello! Is there any better way to do this now? I'd quite like to be able to see 1) the propositions of theorems defined in the current file or 2) the currently available theorems that can be applied to the current goal / active hypotheses. (Though this last one seems difficult.)

[JJ]

The tooling I'm using is VSCode but I'd be interested in answers for Emacs, too.

[Weiyi Wang]

2) sounds like some variant of apply? tactic

[JJ]

Thanks! That's handy. Judging from the time it takes to chug I guess 2) being constantly visually available in ex. the InfoView like goals are isn't a realistic possibility.

[JJ]

For 1), is there any way to have Lean stick that information in a sidebar or something?