<div dir="ltr">I have some running code at <a href="https://github.com/UlfNorell/agda-summer-school/tree/EJCP-solutions">https://github.com/UlfNorell/agda-summer-school/tree/EJCP-solutions</a><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Dec 13, 2014 at 8:44 PM, Sergei Meshveliani <span dir="ltr">&lt;<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On Fri, 2014-12-12 at 15:47 +0100, Philipp Hausmann wrote:<br>
&gt; Hi,<br>
&gt;<br>
&gt; I am looking for example programs to test the Agda compilers. Just by<br>
&gt; searching github, google &amp; co I couldn&#39;t find many Agda programs which<br>
&gt; can actually be run and do something interesting.<br>
</span>&gt; [..]<br>
<br>
<br>
<br>
<a href="http://www.botik.ru/pub/local/Mechveliani/agdaNotes/EuclideanResidue-dec13-2014.zip" target="_blank">http://www.botik.ru/pub/local/Mechveliani/agdaNotes/EuclideanResidue-dec13-2014.zip</a><br>
<br>
 An example of a provable programming of mathematics in a functional<br>
 language with dependent types.<br>
<br>
<br>
See there  README.agda.<br>
<br>
This library is written in Agda<br>
and has been tested under  Agda 2.4.2.2,  MAlonzo, ghc-7.8.3.<br>
<br>
The test  Main.main  performs computations in the domain of<br>
R = Integer modulo m,<br>
namely, performs division for all element pairs in R<br>
(division is a partial map in  R,  it returns the result in the<br>
(Dec _) format).<br>
<br>
The library implements the residue domain  R = E/(b)  for an arbitrary<br>
Euclidean ring  E.<br>
<br>
And the test instance in  Main  is set  E = Integer.<br>
<br>
<br>
Regards,<br>
<br>
------<br>
Sergei<br>
<div class="HOEnZb"><div class="h5"><br>
<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" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>