The MiniAgda package


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.


Versions 0.2014.1.9, 0.2014.5.5, 0.2014.9.12, 0.2016.12.19
Dependencies array (>=0.3 && <0.6), base (>=4.6 && <5), containers (>=0.3 && <0.6), haskell-src-exts (==1.17.*), mtl (>= && <2.3), pretty (>=1.0 && <1.2) [details]
License OtherLicense
Author Andreas Abel and Karl Mehltretter
Maintainer Andreas Abel <>
Stability Unknown
Category Dependent types
Home page
Bug tracker
Source repository head: git clone
Uploaded Tue Dec 20 19:43:51 UTC 2016 by AndreasAbel
Distributions NixOS:0.2016.12.19
Downloads 888 total (31 in the last 30 days)
0 []
Status Docs not available [build log]
Last success reported on 2016-12-21 [all 3 reports]


Maintainer's Corner

For package maintainers and hackage trustees