@hackage dedukti1.1.4

A type-checker for the λΠ-modulo calculus.

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.
  • Installation

    Custom

  • Dependencies (0)

  • Dependents (1)

    @hackage/acme-everything
  • Package Flags

      test
       (off by default)

      Compile test harness (requires test-framework).