@hackage MiniAgda0.2020.4.14

A toy dependently typed programming language with type-based termination.

MiniAgda

A prototypical dependently typed languages with sized types and variances.

Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type

  cabal v1-update
  cabal v1-install alex
  cabal v1-install happy
  cabal v1-install MiniAgda

To build MiniAgda from source, replace the last command with

 make

See directories test/succeed/ and examples/.

Some examples are commented on the (dormant) MiniAgda blog.