[Agda] Getting started: Emacs

[Jason -Zhong Sheng- Hu]

Hi Vox,

to add more resources that I know, Conor McBride uploaded his lectures on Agda on Youtube (CS410): https://www.youtube.com/channel/UCWx63QH5IevL6gsP9stpG_w/search?query=410

I personally have watched all the videos and found them very good. in particular, he talked about not only Agda but also the Emacs gestures he used (though I don't understand why he preferred ascii to unicode).

The Agda doc also has section about Emacs mode: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html

I personally have a very customized Agda setup in Emacs, which I can also share if you are interested.

Thanks,
Jason Hu
https://hustmphrrr.github.io/

________________________________
From: Agda <agda-bounces at lists.chalmers.se> on behalf of Philip Wadler <wadler at inf.ed.ac.uk>
Sent: February 9, 2020 2:45 PM
To: Vox Veritatis <lar307trd at gmail.com>
Cc: Agda mailing list <agda at lists.chalmers.se>
Subject: Re: [Agda] Getting started: Emacs

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.

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se
https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200209/42c705c9/attachment.html>