name: dedukti version: 1.1.4 author: Mathieu Boespflug maintainer: Mathieu Boespflug copyright: © 2009 CNRS - École Polytechnique - INRIA homepage: http://www.lix.polytechnique.fr/dedukti synopsis: A type-checker for the λΠ-modulo calculus. description: Dedukti is a proof checker for the λΠ-modulo calculus, a dependently typed λ-calculus with the addition of typed rewrite rules, capable of expressing proofs in Deduction Modulo [1]. . [1] G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, /Journal of Automated Reasoning/, 31, 2003, pp. 33-72. category: Theorem Provers, Compilers/Interpreters license: GPL license-file: COPYING cabal-version: >= 1.6.0 build-type: Custom tested-with: GHC ==6.10, GHC ==7.0.2 data-files: t/bug.dk t/coc.dk t/coq/Datatypes.dk t/delta1.dk t/delta2.dk t/exemple.dk t/f.dk t/fold/arith.dk t/logic.dk t/nat.dk t/peano.dk t/plus.dk scripts/dkrun extra-source-files: doc/mkfile doc/manual.texi.in doc/fdl.texi doc/references.texi flag test description: Compile test harness (requires test-framework). default: False source-repository head type: git location: git://github.com/mboes/dedukti library exposed-modules: Dedukti.Runtime build-depends: time >= 1.1, unix >= 2.3 extensions: DeriveDataTypeable, PatternGuards, FlexibleInstances ghc-options: -fwarn-unused-binds -fwarn-unused-imports executable dedukti main-is: Dedukti.hs other-modules: Dedukti.Core Dedukti.Parser Dedukti.Parser.External Dedukti.Parser.Prefix Dedukti.Parser.Interface Dedukti.Pretty Dedukti.Driver.Interactive Dedukti.Driver.Batch Dedukti.Driver.Compile Dedukti.Rule Dedukti.DkM Dedukti.Config Dedukti.Module Dedukti.CodeGen Dedukti.CodeGen.Exts Dedukti.Analysis.Rule Dedukti.Analysis.Scope Dedukti.Analysis.Dependency System.Console.Option build-depends: base >= 4 && < 5, mtl >= 1.1, containers >= 0.2, directory, filepath, process, bytestring >= 0.9.1.0, parsec >= 3.1.0, wl-pprint >= 1.0, haskell-src-exts >= 1.1.0, haskell-src-exts-qq >= 0.4, Stream >= 0.3 && < 0.3.2, hmk >= 0.9.7, stringtable-atom >= 0.0.6 extensions: CPP, EmptyDataDecls, PatternGuards, GeneralizedNewtypeDeriving, DeriveDataTypeable, TypeFamilies, LiberalTypeSynonyms, FlexibleInstances, FlexibleContexts, OverloadedStrings, RecordWildCards, TypeSynonymInstances, ScopedTypeVariables MultiParamTypeClasses, TemplateHaskell, QuasiQuotes ghc-options: -fwarn-unused-binds -fwarn-unused-imports executable dedukti-tests main-is: Test.hs if !flag(test) buildable: False else buildable: True build-depends: directory, filepath, process, test-framework >= 0.2 && < 0.3 extensions: DeriveDataTypeable, MultiParamTypeClasses, RecordWildCards ghc-options: -fwarn-unused-binds -fwarn-unused-imports