[Agda] Getting started: Emacs

[Philip Wadler]

My textbook (at plfa.inf.ed.ac.uk) has a few sections on using Agda
interactively from Emacs:
    https://plfa.github.io/Naturals/#writing-definitions-interactively
    https://plfa.github.io/Induction/#building-proofs-interactively
Please let me know if those are helpful to you (or not). Cheers, -- P

.   \ Philip Wadler, Professor of Theoretical Computer Science,
.   /\ School of Informatics, University of Edinburgh
.  /  \ and Senior Research Fellow, IOHK
. http://homepages.inf.ed.ac.uk/wadler/

On Sun, 9 Feb 2020 at 12:42, Vox Veritatis <lar307trd at gmail.com> wrote:
>
> 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!
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.