[Agda] Example Runnable Agda Programs

Matteo Acerbi matteo.acerbi at gmail.com
Fri Dec 12 18:45:03 CET 2014


On Fri, Dec 12, 2014 at 3:47 PM, Philipp Hausmann wrote:
>
> [..]
>
> Long story short, does anyone have actual runnable Agda programs we
> could use for testing?
>
> Cheers,
> Philipp

Hi!

I have a few toy examples using Concurrent Haskell primitives here:

https://github.com/ma82/session

I hope the instructions to build the examples and check their output
are clear enough.

I don't know whether these programs might be interesting for your purpose.

Possibly, the code might be atypical enough to hit some corner cases,
but beware that

1. there are uses of unsafeCoerce
2. termination checking is skipped for the evaluator

If you are interested in compiling this code with your backend and
find some problems, please contact me.

Good luck with your project, thanks for your work!

Cheers,
Matteo


More information about the Agda mailing list