Support folding in the infoview

[Julian]

Via 'foldexpr' presumably.

[chenson2018]

I gave this a little more thought. I think the folds that make sense are the entirety of the type for each hypothesis. I don't think anything more granular is very useful or practical. The tricky part is that ideally folds persist as the infoview changes. A few things that come to mind are:

• hypothesis names(s) that change
• types that change e.g. when unfolding
• multiple hypotheses sharing a type ascription
• how does this interact with pins?
• jumping between different proofs, multiple files, etc.

I don't have a very clear design in mind and imagine there are lots of edge cases, so I'd be interested to hear your thoughts. My first idea is having set(s) of hypothesis names that are currently folded. This set could automatically update to an extent (check existing hypotheses and folds on change), and maybe also support a command for manually updating/resetting. This is probably a little vague/incorrect because I'm not actually familiar with details of how the infoview updates.

Again, if we settle on a design I'm happy to try to work on this myself if you can point me in the general direction of the relevant files. I'll just be a little slow between learning nvim Lua commands and PhD'ing.

[Julian]

Apologies for not getting much time to think about this myself yet (and therefore not responding) -- I appreciate your thoughts and definitely your offer to look into this!

As I say I don't have a super intelligent response yet -- if anything the first thing that I think still occurs to me is that while I agree that folding hypotheses sounds nice, I think starting with goals is actually easier, because as you say hypotheses change more often and in more ways -- whereas perhaps goal folding is easier to reason about under some initial invariants (like "the number of goals hasn't changed" and/or the name of the current goal is the same).

I do think it should be solvable to persist folds across updates, but I think it's also probably fine to initially start playing with very simple things and iterating. I think the same is likely true for your questions about jumping between files -- these seem like good things to figure out but I'd probably start with the bare simplest case(s) first.

I'm still not sure I've given enough help to be helpful! But I will try to think more about this and give more guidance. And yeah thanks again! If you do simply try to start on this given the above, I'd say definitely ping me on a PR once you've written more than 50 lines (or sooner of course if you get stuck) so that we can see how it looks!