[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