[Agda] Example Runnable Agda Programs

[Ulf Norell]

I have some running code at
https://github.com/UlfNorell/agda-summer-school/tree/EJCP-solutions

/ Ulf

On Sat, Dec 13, 2014 at 8:44 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> On Fri, 2014-12-12 at 15:47 +0100, Philipp Hausmann wrote:
> > Hi,
> >
> > I am looking for example programs to test the Agda compilers. Just by
> > searching github, google & co I couldn't find many Agda programs which
> > can actually be run and do something interesting.
> > [..]
>
>
>
>
> http://www.botik.ru/pub/local/Mechveliani/agdaNotes/EuclideanResidue-dec13-2014.zip
>
>  An example of a provable programming of mathematics in a functional
>  language with dependent types.
>
>
> See there  README.agda.
>
> This library is written in Agda
> and has been tested under  Agda 2.4.2.2,  MAlonzo, ghc-7.8.3.
>
> The test  Main.main  performs computations in the domain of
> R = Integer modulo m,
> namely, performs division for all element pairs in R
> (division is a partial map in  R,  it returns the result in the
> (Dec _) format).
>
> The library implements the residue domain  R = E/(b)  for an arbitrary
> Euclidean ring  E.
>
> And the test instance in  Main  is set  E = Integer.
>
>
> Regards,
>
> ------
> Sergei
>
>
>
> _______________________________________________
> 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/20141215/560acbde/attachment.html