Agda-2.2.2: Agda.cabal
name: Agda
version: 2.2.2
cabal-version: >= 1.6 && < 2
build-type: Simple
license: OtherLicense
license-file: LICENSE
author: Ulf Norell, Catarina Coquand, Makoto Takeyama, Nils Anders Danielsson, Andreas Abel, ...
maintainer: Ulf Norell <ulfn@chalmers.se>
homepage: http://wiki.portal.chalmers.se/agda/
bug-reports: http://code.google.com/p/agda/issues/list
category: Dependent types
synopsis: A dependently typed functional programming language and proof assistant
description:
Agda is a dependently typed functional programming language: It has
inductive families, which are like Haskell's GADTs, but they can be
indexed by values and not just types. It also has parameterised
modules, mixfix operators, Unicode characters, and an interactive
Emacs interface (the type checker can assist in the development of
your code).
.
Agda is also a proof assistant: It is an interactive system for
writing and checking proofs. Agda is based on intuitionistic type
theory, a foundational system for constructive mathematics developed
by the Swedish logician Per Martin-Löf. It has many similarities
with other proof assistants based on dependent types, such as Coq,
Epigram and NuPRL.
.
Note that if you want to use the command-line program (agda), then
you should also install the Agda-executable package. This package
includes an Emacs mode for Agda, but you need to set up the Emacs
mode yourself (see the README).
tested-with: GHC == 6.8.3 && == 6.10.2
extra-source-files: src/full/Agda/undefined.h
README
data-dir: src/data
data-files: Agda.css
emacs-mode/*.el
source-repository head
type: darcs
location: http://code.haskell.org/Agda/
source-repository this
type: darcs
location: http://code.haskell.org/Agda/
tag: 2.2.2
library
hs-source-dirs: src/full
build-depends: base >= 3 && < 4,
mtl >= 1.1 && < 2,
QuickCheck == 2.1.0.1,
haskell98 >= 1.0.1 && < 2,
haskell-src >= 1.0.1.1 && < 2,
containers >= 0.1.0 && < 1,
pretty >= 1 && < 2,
directory >= 1 && < 2,
old-time >= 1 && < 2,
bytestring >= 0.9.0.1 && < 1,
array >= 0.1 && < 1,
binary >= 0.4.4 && < 0.6,
zlib >= 0.4.0.1 && < 1,
filepath >= 1.1 && < 2,
process >= 1.0.1.0 && < 2,
haskeline >= 0.3 && < 0.7,
utf8-string >= 0.3 && < 0.4,
xhtml >= 3000.2 && < 3000.3
if impl(ghc >= 6.10)
build-depends: ghc-prim >= 0.1 && < 1
build-tools: happy >= 1.15 && < 2,
alex >= 2.0.1 && < 3
exposed-modules: Agda.Main
Agda.Interaction.BasicOps
Agda.Interaction.GhciTop
Agda.Compiler.Agate.Classify
Agda.Compiler.Agate.Common
Agda.Compiler.Agate.Main
Agda.Compiler.Agate.OptimizedPrinter
Agda.Compiler.Agate.TranslateName
Agda.Compiler.Agate.UntypedPrinter
Agda.Compiler.Alonzo.Main
Agda.Compiler.Alonzo.Names
Agda.Compiler.Alonzo.Haskell
Agda.Compiler.Alonzo.PatternMonad
Agda.Compiler.HaskellTypes
Agda.Compiler.MAlonzo.Compiler
Agda.Compiler.MAlonzo.Encode
Agda.Compiler.MAlonzo.Misc
Agda.Compiler.MAlonzo.Pretty
Agda.Compiler.MAlonzo.Primitives
Agda.Interaction.CommandLine.CommandLine
Agda.Interaction.Exceptions
Agda.Interaction.Highlighting.Emacs
Agda.Interaction.Highlighting.Generate
Agda.Interaction.Highlighting.HTML
Agda.Interaction.Highlighting.Precise
Agda.Interaction.Highlighting.Range
Agda.Interaction.Highlighting.Vim
Agda.Interaction.Imports
Agda.Interaction.MakeCase
Agda.Interaction.Monad
Agda.Interaction.Options
Agda.Syntax.Abstract.Name
Agda.Syntax.Abstract.Pretty
Agda.Syntax.Abstract.Views
Agda.Syntax.Abstract
Agda.Syntax.Common
Agda.Syntax.Concrete.Definitions
Agda.Syntax.Concrete.Name
Agda.Syntax.Concrete.Operators.Parser
Agda.Syntax.Concrete.Operators
Agda.Syntax.Concrete.Pretty
Agda.Syntax.Concrete
Agda.Syntax.Fixity
Agda.Syntax.Info
Agda.Syntax.Internal
Agda.Syntax.Internal.Generic
Agda.Syntax.Internal.Pattern
Agda.Syntax.Literal
Agda.Syntax.Parser.Alex
Agda.Syntax.Parser.Comments
Agda.Syntax.Parser.Layout
Agda.Syntax.Parser.LexActions
Agda.Syntax.Parser.Lexer
Agda.Syntax.Parser.LookAhead
Agda.Syntax.Parser.Monad
Agda.Syntax.Parser.Parser
Agda.Syntax.Parser.StringLiterals
Agda.Syntax.Parser.Tokens
Agda.Syntax.Parser
Agda.Syntax.Position
Agda.Syntax.Scope.Base
Agda.Syntax.Scope.Monad
Agda.Syntax.Strict
Agda.Syntax.Translation.AbstractToConcrete
Agda.Syntax.Translation.ConcreteToAbstract
Agda.Syntax.Translation.InternalToAbstract
Agda.Termination.CallGraph
Agda.Termination.Lexicographic
Agda.Termination.Matrix
Agda.Termination.Semiring
Agda.Termination.TermCheck
Agda.Termination.Termination
Agda.Tests
Agda.TypeChecker
Agda.TypeChecking.Abstract
Agda.TypeChecking.Constraints
Agda.TypeChecking.Conversion
Agda.TypeChecking.Coverage
Agda.TypeChecking.Coverage.Match
Agda.TypeChecking.DisplayForm
Agda.TypeChecking.Empty
Agda.TypeChecking.EtaContract
Agda.TypeChecking.Errors
Agda.TypeChecking.Free
Agda.TypeChecking.Implicit
Agda.TypeChecking.Injectivity
Agda.TypeChecking.MetaVars
Agda.TypeChecking.Monad.Base
Agda.TypeChecking.Monad.Builtin
Agda.TypeChecking.Monad.Closure
Agda.TypeChecking.Monad.Constraints
Agda.TypeChecking.Monad.Context
Agda.TypeChecking.Monad.Debug
Agda.TypeChecking.Monad.Env
Agda.TypeChecking.Monad.Exception
Agda.TypeChecking.Monad.Imports
Agda.TypeChecking.Monad.MetaVars
Agda.TypeChecking.Monad.Mutual
Agda.TypeChecking.Monad.Open
Agda.TypeChecking.Monad.Options
Agda.TypeChecking.Monad.Signature
Agda.TypeChecking.Monad.SizedTypes
Agda.TypeChecking.Monad.State
Agda.TypeChecking.Monad.Statistics
Agda.TypeChecking.Monad.Trace
Agda.TypeChecking.Monad
Agda.TypeChecking.Patterns.Match
Agda.TypeChecking.Polarity
Agda.TypeChecking.Positivity
Agda.TypeChecking.Pretty
Agda.TypeChecking.Primitive
Agda.TypeChecking.Rebind
Agda.TypeChecking.Records
Agda.TypeChecking.Reduce
Agda.TypeChecking.Rules.Builtin
Agda.TypeChecking.Rules.Data
Agda.TypeChecking.Rules.Decl
Agda.TypeChecking.Rules.Def
Agda.TypeChecking.Rules.LHS
Agda.TypeChecking.Rules.LHS.Implicit
Agda.TypeChecking.Rules.LHS.Instantiate
Agda.TypeChecking.Rules.LHS.Problem
Agda.TypeChecking.Rules.LHS.Split
Agda.TypeChecking.Rules.LHS.Unify
Agda.TypeChecking.Rules.Record
Agda.TypeChecking.Rules.Term
Agda.TypeChecking.Serialise
Agda.TypeChecking.SizedTypes
Agda.TypeChecking.Substitute
Agda.TypeChecking.Telescope
Agda.TypeChecking.Test.Generators
Agda.TypeChecking.Tests
Agda.TypeChecking.With
Agda.Utils.Char
Agda.Utils.Either
Agda.Utils.FileName
Agda.Utils.Fresh
Agda.Utils.Function
Agda.Utils.Generics
Agda.Utils.Graph
Agda.Utils.Hash
Agda.Utils.Impossible
Agda.Utils.IO
Agda.Utils.List
Agda.Utils.Map
Agda.Utils.Maybe
Agda.Utils.Monad.Undo
Agda.Utils.Monad
Agda.Utils.Permutation
Agda.Utils.Pointer
Agda.Utils.Pretty
Agda.Utils.QuickCheck
Agda.Utils.ReadP
Agda.Utils.SemiRing
Agda.Utils.Serialise
Agda.Utils.Size
Agda.Utils.String
Agda.Utils.Suffix
Agda.Utils.TestHelpers
Agda.Utils.Trace
Agda.Utils.Trie
Agda.Utils.Tuple
Agda.Utils.Unicode
Agda.Utils.Warshall
Agda.Version
other-modules: Paths_Agda
ghc-options: -auto-all -w -Werror -fwarn-dodgy-imports
-fwarn-duplicate-exports -fwarn-hi-shadowing
-fwarn-incomplete-patterns -fwarn-missing-fields
-fwarn-missing-methods -fwarn-overlapping-patterns
if impl(ghc >= 6.10)
ghc-options: -fwarn-warnings-deprecations -fwarn-deprecated-flags
-fwarn-dodgy-foreign-imports
executable agda-mode
hs-source-dirs: src/agda-mode
main-is: Main.hs
other-modules: Paths_Agda
build-depends: base >= 3 && < 4,
filepath >= 1.1 && < 2,
process >= 1.0.1.0 && < 2,
utf8-string >= 0.3 && < 0.4