hackage.haskell.org : MiniAgda
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.
Registry
- Homepage
- JSON
- codemeta.json
purl: pkg:hackage/MiniAgda
Keywords:
dependent-types
, library
, mit
, program
, Propose Tags
License: MIT
Latest release: 7 months ago
First release: about 12 years ago
Dependent repositories: 1
Downloads: 7,555 total
Last synced: about 1 month ago