name: hol
version: 1.4
category: Logic
synopsis: Higher order logic
license: MIT
license-file: LICENSE
cabal-version: >= 1.10
build-type: Simple
extra-source-files: README.md doc/axioms.txt doc/bool.txt test/bool.art test/bool.int test/bool.thy test/bool-def.art
extra-tmp-files: hol-profile.aux hol-profile.hp hol-profile.pdf hol-profile.prof hol-profile.ps
author: Joe Leslie-Hurd <joe@gilith.com>
maintainer: Joe Leslie-Hurd <joe@gilith.com>
description:
  This package implements a higher order logic kernel with OpenTheory support.

Library
  build-depends:
    base >= 4.0 && < 5.0,
    bytestring >= 0.9,
    containers >= 0.5,
    filepath >= 1.3,
    parsec >= 3.1,
    pretty >= 1.1,
    process >= 1.2,
    text >= 0.11,
    transformers >= 0.3
  default-language: Haskell2010
  hs-source-dirs: src
  ghc-options: -Wall
  exposed-modules:
    HOL.Const
    HOL.Conv
    HOL.Data
    HOL.Name
    HOL.OpenTheory
    HOL.OpenTheory.Article
    HOL.OpenTheory.Interpret
    HOL.OpenTheory.Package
    HOL.Parse
    HOL.Print
    HOL.Rule
    HOL.Sequent
    HOL.Subst
    HOL.Term
    HOL.TermAlpha
    HOL.TermData
    HOL.Theory
    HOL.Thm
    HOL.Type
    HOL.TypeData
    HOL.TypeOp
    HOL.TypeSubst
    HOL.TypeVar
    HOL.Util
    HOL.Var

executable hol-pkg
  build-depends:
    base >= 4.0 && < 5.0,
    bytestring >= 0.9,
    containers >= 0.5,
    filepath >= 1.3,
    parsec >= 3.1,
    pretty >= 1.1,
    process >= 1.2,
    text >= 0.11,
    transformers >= 0.3
  default-language: Haskell2010
  hs-source-dirs: src
  ghc-options: -Wall -threaded "-with-rtsopts=-N" -rtsopts
  main-is: Main.hs
  other-modules:
    HOL.Const
    HOL.Conv
    HOL.Data
    HOL.Name
    HOL.OpenTheory
    HOL.OpenTheory.Article
    HOL.OpenTheory.Interpret
    HOL.OpenTheory.Package
    HOL.Parse
    HOL.Print
    HOL.Rule
    HOL.Sequent
    HOL.Subst
    HOL.Term
    HOL.TermAlpha
    HOL.TermData
    HOL.Theory
    HOL.Thm
    HOL.Type
    HOL.TypeData
    HOL.TypeOp
    HOL.TypeSubst
    HOL.TypeVar
    HOL.Util
    HOL.Var

test-suite hol-test
  type: exitcode-stdio-1.0
  build-depends:
    base >= 4.0 && < 5.0,
    bytestring >= 0.9,
    containers >= 0.5,
    filepath >= 1.3,
    parsec >= 3.1,
    pretty >= 1.1,
    process >= 1.2,
    QuickCheck >= 2.4,
    text >= 0.11,
    transformers >= 0.3
  default-language: Haskell2010
  hs-source-dirs: src
  ghc-options: -Wall
  main-is: Test.hs
  other-modules:
    HOL.Const
    HOL.Conv
    HOL.Data
    HOL.Name
    HOL.OpenTheory
    HOL.OpenTheory.Article
    HOL.OpenTheory.Interpret
    HOL.OpenTheory.Package
    HOL.Parse
    HOL.Print
    HOL.Rule
    HOL.Sequent
    HOL.Subst
    HOL.Term
    HOL.TermAlpha
    HOL.TermData
    HOL.Theory
    HOL.Thm
    HOL.Type
    HOL.TypeData
    HOL.TypeOp
    HOL.TypeSubst
    HOL.TypeVar
    HOL.Util
    HOL.Var

benchmark hol-profile
  type: exitcode-stdio-1.0
  build-depends:
    base >= 4.0 && < 5.0,
    bytestring >= 0.9,
    containers >= 0.5,
    filepath >= 1.3,
    parsec >= 3.1,
    pretty >= 1.1,
    process >= 1.2,
    text >= 0.11,
    transformers >= 0.3
  default-language: Haskell2010
  hs-source-dirs: src
  ghc-options:
    -Wall
    -fprof-auto-exported
    "-with-rtsopts=-p -s -h -i0.1"
  main-is: Profile.hs
  other-modules:
    HOL.Const
    HOL.Conv
    HOL.Data
    HOL.Name
    HOL.OpenTheory
    HOL.OpenTheory.Article
    HOL.OpenTheory.Interpret
    HOL.OpenTheory.Package
    HOL.Parse
    HOL.Print
    HOL.Rule
    HOL.Sequent
    HOL.Subst
    HOL.Term
    HOL.TermAlpha
    HOL.TermData
    HOL.Theory
    HOL.Thm
    HOL.Type
    HOL.TypeData
    HOL.TypeOp
    HOL.TypeSubst
    HOL.TypeVar
    HOL.Util
    HOL.Var

source-repository head
  type: git
  location: git://github.com/gilith/hol.git