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.

[maintain] [Publish]

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]


Versions 0.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.2019.3.29, 0.2019.12.13, 0.2020.4.14, 0.2022.3.11, 0.2022.3.11
Change log CHANGELOG
Dependencies array (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.7), haskell-src-exts (>=1.21 && <1.22), mtl (>=2.2.2 && <2.4), pretty (>=1.0 && <1.2), transformers [details]
License MIT
Author Andreas Abel and Karl Mehltretter
Maintainer Andreas Abel <>
Category Dependent types
Home page
Bug tracker
Source repo head: git clone
Uploaded by AndreasAbel at 2022-03-11T16:03:11Z


Maintainer's Corner

For package maintainers and hackage trustees

Readme for MiniAgda-0.2022.3.11

[back to package description]


Cabal build Hackage

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



See directories test/succeed/ and examples/.

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