[Agda] Example Runnable Agda Programs

[Sergei Meshveliani]

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