@hackage MiniAgda0.2022.3.11

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 or via ghcup. In a shell, type

  cabal update
  cabal 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.