Stream: VsCoq devs & users

Topic: Summary of lemmas in a coq file

Mycroft92 (Jan 30 2023 at 10:02):

Hi,
Is there a convenient way to check the lemmas/theorems in a file in vscoq? I have a setup with 1-2K lines per file and over 30 results and I just want to look at the types (theorem statements) without scrolling back and forth. Just wanted to verify with the community before I write a script to do the same.
Thanks,
Madhukar

Huỳnh Trần Khanh (Jan 30 2023 at 10:12):

You can fold all code blocks.

Huỳnh Trần Khanh (Jan 30 2023 at 10:13):

Ctrl+Shift+P then search for this option. I don't remember the exact wording.

Mycroft92 (Jan 30 2023 at 10:17):

Huỳnh Trần Khanh said:

You can fold all code blocks.

Thanks. It works but not perfectly, if the statement is on the next line it gets folded as well image.png

Huỳnh Trần Khanh (Jan 30 2023 at 10:31):

I don't remember the key combination for folding a code block. But you can do this: right click the word "Proof" and choose something that is along the lines of select all occurrences. Then hit the collapse code block key combo to collapse all Proof blocks.

Last updated: Jun 04 2023 at 22:30 UTC