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.