<html><head><meta http-equiv="content-type" content="text/html; charset=utf-8"></head><body dir="auto"><div>There’s a list of tutorials in the Agda docs, to: <a href="https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html">https://agda.readthedocs.io/en/v2.6.0.1/getting-started/tutorial-list.html</a></div><div><br></div><div>In addition to Phil’s and Conor’s, I found Thorsten Altenkirch’s to be really useful.</div><div><br></div><div>Bill</div><br><div dir="ltr"><br>On Feb 9, 2020, at 3:10 PM, Jason -Zhong Sheng- Hu <<a href="mailto:fdhzs2010@hotmail.com">fdhzs2010@hotmail.com</a>> wrote:<br><br></div><blockquote type="cite"><div dir="ltr">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
Hi Vox,</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
to add more resources that I know, Conor McBride uploaded his lectures on Agda on Youtube (CS410):
<a href="https://www.youtube.com/channel/UCWx63QH5IevL6gsP9stpG_w/search?query=410" style="" id="LPNoLP977119">
https://www.youtube.com/channel/UCWx63QH5IevL6gsP9stpG_w/search?query=410</a><br>
</div>
<br>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
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).</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
The Agda doc also has section about Emacs mode: <a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html" style="" id="LPNoLP693101">
https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html</a><br>
</div>
<br>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0); background-color: rgb(255, 255, 255);">
I personally have a very customized Agda setup in Emacs, which I can also share if you are interested.<br>
</div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<div id="Signature">
<div></div>
<div id="divtagdefaultwrapper" dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Thanks,</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b>Jason Hu</b></font></div>
<div dir="ltr" style="font-size: 12pt; color: rgb(0, 0, 0); font-family: Calibri, Arial, Helvetica, sans-serif;">
<font size="3"><b><a href="https://hustmphrrr.github.io/" style="">https://hustmphrrr.github.io/</a></b></font><br>
<font size="3"><b></b></font><font style="font-size:12pt" size="3"><span style="color: rgb(69, 129, 142);"><span style="font-family:trebuchet ms,sans-serif"><b><a target="_blank" style=""></a></b></span></span></font></div>
<div>
<div id="appendonsend"></div>
<div style="font-family: Calibri, Helvetica, sans-serif; font-size: 12pt; color: rgb(0, 0, 0);">
<br>
</div>
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size: 11pt;" data-ogsc="" face="Calibri, sans-serif" color="#000000"><b>From:</b> Agda <<a href="mailto:agda-bounces@lists.chalmers.se">agda-bounces@lists.chalmers.se</a>> on behalf of Philip Wadler <<a href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a>><br>
<b>Sent:</b> February 9, 2020 2:45 PM<br>
<b>To:</b> Vox Veritatis <<a href="mailto:lar307trd@gmail.com">lar307trd@gmail.com</a>><br>
<b>Cc:</b> Agda mailing list <<a href="mailto:agda@lists.chalmers.se">agda@lists.chalmers.se</a>><br>
<b>Subject:</b> Re: [Agda] Getting started: Emacs</font>
<div> </div>
</div>
<div class="BodyFragment"><font size="2"><span style="font-size:11pt">
<div class="PlainText">My textbook (at <a href="http://plfa.inf.ed.ac.uk">plfa.inf.ed.ac.uk</a>) has a few sections on using Agda<br>
interactively from Emacs:<br>
<a href="https://plfa.github.io/Naturals/#writing-definitions-interactively" style="">
https://plfa.github.io/Naturals/#writing-definitions-interactively</a><br>
<a href="https://plfa.github.io/Induction/#building-proofs-interactively" style="">
https://plfa.github.io/Induction/#building-proofs-interactively</a><br>
Please let me know if those are helpful to you (or not). Cheers, -- P<br>
<br>
. \ Philip Wadler, Professor of Theoretical Computer Science,<br>
. /\ School of Informatics, University of Edinburgh<br>
. / \ and Senior Research Fellow, IOHK<br>
. <a href="http://homepages.inf.ed.ac.uk/wadler/" style="">http://homepages.inf.ed.ac.uk/wadler/</a><br>
<br>
On Sun, 9 Feb 2020 at 12:42, Vox Veritatis <<a href="mailto:lar307trd@gmail.com">lar307trd@gmail.com</a>> wrote:<br>
><br>
> Hi all,<br>
><br>
> 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...<br>
><br>
> 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.<br>
><br>
> Any help would be appreciated!<br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" style="">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br>
-- <br>
The University of Edinburgh is a charitable body, registered in<br>
Scotland, with registration number SC005336.<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" style="">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div>
</span></font></div>
</div>
</div>
</div></blockquote><blockquote type="cite"><div dir="ltr"><span>_______________________________________________</span><br><span>Agda mailing list</span><br><span><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a></span><br><span><a href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a></span><br></div></blockquote></body></html>