[Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types

Andreas Abel andreas.abel at ifi.lmu.de
Thu Jan 9 19:39:43 CET 2014


For what it's worth, I finally uploaded MiniAgda to hackage.  If you 
want to play around with type-based termination and coinduction in a 
dependently-typed setting, try:

   cabal install MiniAgda

Some examples and pointers to literature are (still) on my old homepage:

   http://www2.tcs.ifi.lmu.de/~abel/miniagda/

Source code and issue tracker are on the darcs hub:

   http://hub.darcs.net/abel/miniagda/

Have fun playing (or despair of the horrible error messages),
and have a happy new year,

Andreas

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.



More information about the Agda mailing list