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 [RSS] [faq]||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|
|Dependencies||array (>=0.3 && <0.6), base (>=4.6 && <4.11), containers (>=0.3 && <0.6), haskell-src-exts (==1.17.*), mtl (>=18.104.22.168 && <2.3), pretty (>=1.0 && <1.2) [details]|
|Author||Andreas Abel and Karl Mehltretter|
|Maintainer||Andreas Abel <email@example.com>|
|Revised||Revision 1 made by HerbertValerioRiedel at 2018-02-01T11:51:51Z|
|Source repo||head: git clone https://github.com/andreasabel/miniagda|
|Uploaded||by AndreasAbel at 2017-02-18T20:36:25Z|
|Downloads||6285 total (34 in the last 30 days)|
|Rating||2.0 (votes: 1) [estimated by Bayesian average]|
Docs not available [build log]
Last success reported on 2017-02-18 [all 3 reports]
- MiniAgda-0.2017.2.18.tar.gz [browse] (Cabal source package)
- Package description (revised from the package)
Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.