[Agda] Hiding parts of proofs in Emacs Agda mode?

[Jonathan Steven Prieto Cubides]

Hi Erik,


If you use the Atom editor and the add-on Agda Mode, that's

what you want is possible. Just use indentation if you want to hide

parts of the code. Atom allows you to fold or unfold all the code

at some level of indentation.


https://github.com/banacorn/agda-mode


Jonathan

________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Erik Palmgren <palmgren at math.su.se>
Sent: Friday, February 1, 2019 11:47:13 AM
To: Agda at lists.chalmers.se
Subject: [Agda] Hiding parts of proofs in Emacs Agda mode?



Does any know if there is some way of temporarily hiding parts of proofs in

Emacs Agda mode? Maybe some general feature of Emacs can do that?


For instance, it would be useful to hide definiens/proofs when browsing

Agda files.


I seem to recall that there was such a feature in Alfa a GUI for Agda 1, which

was very useful . In e.g. Mathematica there is also a convenient section system,

where parts can be hidden or folded away with a click.



Erik