<div dir="ltr"><div>Hi all,</div><div><br></div><div>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...</div><div><br></div><div>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.</div><div><br></div><div>Any help would be appreciated!</div></div>