@hackage uAgda1.1.0.0

A simplistic dependently-typed language with parametricity.

uAgda implements an experimental dependently-typed language (and proof assistant by the Curry-Howard isomorphism). The goal of the project is twofold:

  1. Experiment with a minimalistic language that is strong enough to program and reason in.

  2. Give a simple implementation of its type-checker (ours is ~200 lines).

See the share/tutorial directory for how to get started.