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

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.


MiniAgda is a tiny dependently-typed programming language in the style of Agda. It serves as a laboratory to test potential additions to the language and type system of Agda. MiniAgda's termination checker is a fusion of sized types and size-change termination and supports coinduction. Equality incorporates eta-expansion at record and singleton types. Function arguments can be declared as static; such arguments are discarded during equality checking and compilation. Recent features include bounded size quantification and destructor patterns for a more general handling of coinduction.

[Skip to ReadMe]


Versions0.2014.1.9, 0.2014.5.5, 0.2014.9.12, 0.2016.12.19, 0.2017.2.18, 0.2018.11.4, 0.2018.11.6, 0.2018.11.6
Dependenciesarray (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.6), haskell-src-exts (>=1.20 && <2.0), mtl (>=2.2.2 && <2.3), pretty (>=1.0 && <1.2) [details]
AuthorAndreas Abel and Karl Mehltretter
MaintainerAndreas Abel <>
CategoryDependent types
Home page
Bug tracker
Source repositoryhead: git clone
UploadedTue Nov 6 08:11:47 UTC 2018 by AndreasAbel


Maintainers' corner

For package maintainers and hackage trustees

Readme for MiniAgda-0.2018.11.6

[back to package description]


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 update
  cabal install alex
  cabal install happy
  cabal install MiniAgda


See test/succeed/ and examples/