[Agda] Getting started: Emacs

[william.lawrence.harrison at gmail.com]

There’s a list of tutorials in the Agda docs, to: https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html

In addition to Phil’s and Conor’s, I found Thorsten Altenkirch’s to be really useful.

Bill


> On Feb 9, 2020, at 3:10 PM, Jason -Zhong Sheng- Hu <fdhzs2010 at hotmail.com> wrote:
> 
> 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
> _______________________________________________
> 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/18f3a8e6/attachment.html>