[Agda] Getting started: Emacs

[Vox Veritatis]

Hi all,

Is there any video (or some other kind of information) on how to use Emacs
when writing proofs in Agda? I seem to only find PDF documents about the
proof language plus several videos on the same topic. But nothing about how
to use Emacs to make progress. For example: suppose one writes a partial
proof, how does one see the status? What goals are closed? What is the
binding engine supposed to be? Can I set that once and for all, instead of
being asked about it all the time? This kind of stuff...

For a newcomer to both Emacs and Agda, having to deal with the interface
might be more of a challenge than the proof language itself.

Any help would be appreciated!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200209/f9512640/attachment.html>