a couple of possible feature requests

Stream: lean4

[Paige Thomas]

I was wondering if I could make a couple of feature requests, if there aren't existing ways to achieve the same goals.

Would it be possible to have a window with a list of the definitions and theorems that have been proven in the current file, or list of files in the current repo, where just the statements of the definitions and theorems are shown, and some way to filter on it? I often find myself scrolling up and down through the file I am working on to recall what I proved and what the name of the theorem was.

Would it also be possible to have a button to copy the list of current goals to the clipboard?

[James Sully]

For the first one, if you're using vscode, hit ctrl-shift-o for a list of definitions

[James Sully]

it doesn't include the types unfortunately.

[Paige Thomas]

Nice. I can put it in a side window and scroll through them. Thank you.