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.