[Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and
sized types
gallais
guillaume.allais at strath.ac.uk
Fri Jan 10 01:01:24 CET 2014
And if you want syntax highlighting and a "please typecheck" command
à la Agda in emacs (i.e. bound to C-c C-l), you can have a look here:
https://github.com/gallais/MiniAgda-mode
On 09/01/14 18:39, Andreas Abel wrote:
> 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
>
More information about the Agda
mailing list