@hackage / uAgda

A simplistic dependently-typed language with parametricity.

Latest1.2.0.4

About

Metadata

  • Last updated , by JeanPhilippeBernardy
  • License LicenseRef-OtherLicense
  • Maintained by: jeanphilippe.bernardy@gmail.com

  • Lottery factor: 0

Links

Installation

Readme

uAgda implements an experimental dependently-typed language (and proof assistant by the Curry-Howard isomorphism), extended with support for parametricity.

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