coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: gallais <guillaume.allais AT strath.ac.uk>
To: Andreas Abel <andreas.abel AT ifi.lmu.de>
Cc: haskell-cafe <haskell-cafe AT haskell.org>, Agda List <agda AT lists.chalmers.se>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] [Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types
Date: Fri, 10 Jan 2014 00:01:24 +0000

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

[Coq-Club] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types, Andreas Abel, 01/09/2014
- Re: [Coq-Club] [Agda] ANN: MiniAgda-0.2014.1.9 Toy language with dependent and sized types, gallais, 01/10/2014