Zulip Chat Archive

Stream: lean4

Topic: default infoview filter

Patrick Massot (May 23 2023 at 21:09):

Is there any way to tell VSCode that in a given project I want to filter out hidden assumptions by default in the infoview?

Patrick Massot (May 23 2023 at 21:19):

Let me ping @Wojciech Nawrocki just in case.

Wojciech Nawrocki (May 24 2023 at 09:20):

Hi! There's no option for it afair, but it would be easy to add one.

Last updated: Dec 20 2023 at 11:08 UTC