<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"> P {margin-top:0;margin-bottom:0;} </style>
</head>
<body dir="ltr">
<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 <agda-bounces@lists.chalmers.se> on behalf of Philip Wadler <wadler@inf.ed.ac.uk><br>
<b>Sent:</b> February 9, 2020 2:45 PM<br>
<b>To:</b> Vox Veritatis <lar307trd@gmail.com><br>
<b>Cc:</b> Agda mailing list <agda@lists.chalmers.se><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 plfa.inf.ed.ac.uk) 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 <lar307trd@gmail.com> 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>
> Agda@lists.chalmers.se<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>
Agda@lists.chalmers.se<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>
</body>
</html>