<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"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></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>
> Hi,<br>
><br>
> I am looking for example programs to test the Agda compilers. Just by<br>
> searching github, google & co I couldn't find many Agda programs which<br>
> can actually be run and do something interesting.<br>
</span>> [..]<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>