name:           uAgda
version:        1.0.0.2
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).
        .
        See the share/tutorial directory for how to get started.
   
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

data-files:
     tutorial/00-Start-Here.ua
     tutorial/01-Module.ua
     tutorial/02-Holes.ua
     tutorial/02.1-Relevance.ua
     tutorial/03-Parametricity.ua
     tutorial/03.1-Parametricity-Use.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.*