uAgda-1.0.0.0: uAgda.cabal
name: uAgda
version: 1.0.0.0
category: Dependent Types
synopsis: A simplistic dependently-typed language with parametricity.
description:
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).
license: OtherLicense
-- Creative Commons Attribution Share-Alike
license-file: LICENSE
author: Jean-Philippe Bernardy
maintainer: jeanphilippe.bernardy@gmail.com
Cabal-Version: >= 1.8
tested-with: GHC==6.12.3
build-type: Simple
extra-source-files:
tutorial/00-Start-Here.ua
tutorial/01-Module.ua
tutorial/02-Holes.ua
tutorial/03-Parametricity.ua
tutorial/04-Data.ua
executable uAgda
extensions: CPP, FlexibleInstances, OverloadedStrings
main-is: Main.hs
other-modules:
AbsSynToTerm
Basics
Display
Main
Normal
Options
RawSyntax
Terms
TypeCheckerNF
build-depends: base==4.*
build-depends: cmdargs==0.6.*
build-depends: containers==0.3.*
build-depends: pretty==1.0.*
build-depends: parsec==2.1.*
build-depends: BNFC-meta==0.1.*
build-depends: transformers == 0.2.*
build-depends: monads-fd == 0.1.*