name:                twee
version:             0.1
x-revision: 1
synopsis:            An equational theorem prover
homepage:            http://github.com/nick8325/twee
license:             BSD3
license-file:        LICENSE
author:              Nick Smallbone
maintainer:          nicsma@chalmers.se
category:            Theorem Provers
build-type:          Simple
cabal-version:       >=1.10
extra-source-files:  README src/errors.h tests/*.p
description:
   Twee is an experimental equational theorem prover based on
   Knuth-Bendix completion.
   .
   Given a set of equational axioms and a set of equational
   conjectures it will try to prove the conjectures.
   It will terminate if the conjectures are true but normally
   fail to terminate if they are false.
   .
   The input problem should be in TPTP format (see
   http://www.tptp.org). You can use types and quantifiers, but apart
   from that the problem must be equational.

source-repository head
  type:     git
  location: git://github.com/nick8325/twee.git
  branch:   master

library
  exposed-modules:
    Twee
    Twee.Array
    Twee.Base
    Twee.Pretty
    Twee.Constraints
    Twee.Index
    Twee.Indexes
    Twee.Queue
    Twee.Rule
    Twee.Term
    Twee.Term.Core
    Twee.Utils
    Twee.KBO
    Twee.LPO
    Twee.Label
  build-depends:
    base >= 4 && < 5,
    containers,
    transformers,
    dlist,
    pretty,
    heaps,
    ghc-prim,
    primitive,
    reflection,
    array
  hs-source-dirs:      src
  include-dirs:        src
  ghc-options:         -W -fno-warn-incomplete-patterns -fno-full-laziness
  default-language:    Haskell2010

executable twee
  main-is:             executable/Main.hs
  default-language:    Haskell2010
  build-depends:       base,
                       twee,
                       containers,
                       transformers,
                       pretty,
                       array,
                       reflection,
                       split,
                       jukebox == 0.2.17
  ghc-options:         -W -fno-warn-incomplete-patterns -fno-full-laziness