collapsing have and let declarations in proofs

Stream: lean4

[Shreyas Srinivas]

Is it possible to configure the extension to make have and let declarations collapsible? Inside proofs, it seems as if one doesn't even need to see anything other than have <name> : and an error or warning if that intermediate proof is incomplete or sorried, since the prop will show up on infoview

[Rida Hamadani]

This would be awesome!
Usually in other languages, I can collapse code regions for { and }, in lean, I think it would be great if we can have the same feature but for centered dots and indentation.

[Shreyas Srinivas]

I should add an update. Sometimes these expressions are collapsible and sometimes they are not. Code folding for have and let seems inconsistent. I had two nearly identical (but ugly and long) proofs. Folding worked for one but not the other. Not sure how to reliably reproduce this issue.