The MiniAgda package

[Tags: program]

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

Versions0.2014.1.9, 0.2014.5.5
Dependenciesarray (>=0.3 && <0.6), base (>=4.2 && <4.8), containers (>=0.3 && <0.6), haskell-src-exts (==1.14.*), IfElse (>=0.85 && <2.0), mtl (==2.0.*), pretty (>=1.0 && <1.2) or
array (>=0.3 && <0.6), base (>=4.2 && <4.8), containers (>=0.3 && <0.6), haskell-src-exts (==1.14.*), IfElse (>=0.85 && <2.0), mtl (>=2.1.1 && <2.2), pretty (>=1.0 && <1.2)
LicenseOtherLicense
AuthorAndreas Abel and Karl Mehltretter
MaintainerAndreas Abel <andreas.abel@ifi.lmu.de>
CategoryDependent types
Home pagehttp://www.tcs.ifi.lmu.de/~abel/miniagda/
Bug trackerhttp://hub.darcs.net/abel/miniagda/issues
Source repositoryhead: darcs get http://hub.darcs.net/abel/miniagda
Executablesminiagda
Upload dateMon May 5 14:09:31 UTC 2014
Uploaded byAndreasAbel
Downloads164 total (25 in last 30 days)

Downloads

Maintainers' corner

For package maintainers and hackage trustees