name: twee-lib version: 2.3.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 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. . This package contains only the library part of twee. source-repository head type: git location: git://github.com/nick8325/twee.git branch: master flag llvm description: Build using LLVM backend for faster code. default: False flag bounds-checks description: Use bounds checks for all array operations. default: False library exposed-modules: Twee Twee.Base Twee.Constraints Twee.CP Twee.Equation Twee.Index Twee.Join Twee.KBO Twee.Label Twee.PassiveQueue Twee.Pretty Twee.Proof Twee.Rule Twee.Rule.Index Twee.Term Twee.Task Twee.Utils other-modules: Data.ChurchList Data.DynamicArray Data.Heap Twee.Term.Core build-depends: base >= 4 && < 4.15, containers >= 0.5.11, transformers, dlist, pretty >= 1.1.2.0, ghc-prim, primitive >= 0.7.1.0, vector, uglymemo, random hs-source-dirs: . ghc-options: -W -fno-warn-incomplete-patterns default-language: Haskell2010 if flag(llvm) cpp-options: -DUSE_LLVM if flag(bounds-checks) cpp-options: -DBOUNDS_CHECKS exposed-modules: Data.Primitive.SmallArray.Checked Data.Primitive.ByteArray.Checked Data.Primitive.Checked