The MiniAgda package

[ Tags: dependent-types, program ] [ Propose Tags ]

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.

Properties

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.6), base (>=4.6 && <4.11), containers (>=0.3 && <0.6), haskell-src-exts (==1.17.*), mtl (>=2.2.0.1 && <2.3), pretty (>=1.0 && <1.2) [details]
License OtherLicense
Author Andreas Abel and Karl Mehltretter
Maintainer Andreas Abel <andreas.abel@ifi.lmu.de>
Category Dependent types
Home page http://www.tcs.ifi.lmu.de/~abel/miniagda/
Bug tracker https://github.com/andreasabel/miniagda/issues
Source repo head: git clone https://github.com/andreasabel/miniagda
Uploaded Sat Feb 18 20:36:25 UTC 2017 by AndreasAbel
Updated Thu Feb 1 11:51:51 UTC 2018 by HerbertValerioRiedel to revision 1   [What is this?]
Distributions NixOS:0.2017.2.18
Executables miniagda
Downloads 1766 total (55 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2017-02-18 [all 3 reports]
Hackage Matrix CI

Downloads

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'.

Maintainer's Corner

For package maintainers and hackage trustees