Stream: VsCoq devs & users

Topic: Summary of lemmas in a coq file


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

view this post on Zulip Huỳnh Trần Khanh (Jan 30 2023 at 10:12):

You can fold all code blocks.

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

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

view this post on Zulip 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: Nov 29 2023 at 04:01 UTC