MiniAgda: A toy dependently typed programming language with type-based termination.
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, 0.2017.2.18|
|Dependencies||array (>=0.3 && <0.5), base (>=4.2 && <4.7), containers (>=0.3 && <0.6), haskell-src-exts (==1.14.*), IfElse (>=0.85 && <2.0), mtl (==2.0.* || >=2.1.1 && <2.2), pretty (>=1.0 && <1.2) [details]|
|Author||Andreas Abel and Karl Mehltretter|
|Maintainer||Andreas Abel <email@example.com>|
|Source repo||head: darcs get http://hub.darcs.net/abel/miniagda|
|Uploaded||by AndreasAbel at Thu Jan 9 18:08:51 UTC 2014|
|Downloads||1798 total (10 in the last 30 days)|
|Rating||(no votes yet) [estimated by rule of succession]|
|Status||Docs not available [build log]
Successful builds reported [all 8 reports]
Hackage Matrix CI
For package maintainers and hackage trustees