package lambdapi

Build not yet checked
  1. Overview
  2. No Docs
Proof assistant for the λΠ-calculus modulo rewriting

Install 

dune-project
 Dependency

github.com Edit opam file Versions (13)

Authors

  1. D
    Deducteam and friends

Maintainers

  1. D
    dedukti-dev@inria.fr

Sources

lambdapi-4.0.0.tbz
sha256=0e2e73e0ea0c674f1263bf85ed3453ed3d6084d38eea29974a03ba9e382d29d7
sha512=2831db57fcd09206687a92fc9ee7d363e87bcec5167949e9c8161d41c63d5887b9f3556bfd63a7a9a0c12e5a5dc61a397baf4f496ebdb2a2fce122142c05e7a1

Description

Lambdapi is an interactive proof assistant for the λΠ-calculus modulo rewriting. It can call external automated theorem provers via Why3. The user manual is on https://lambdapi.readthedocs.io/. A standard library and other developments are available on https://github.com/Deducteam/opam-lambdapi-repository/. An extension for Emacs is available on MELPA. An extension for VSCode is available on the VSCode Marketplace. Lambdapi can read Dedukti files. It includes checkers for local confluence and subject reduction. It also provides commands to export Lambdapi files to other formats or systems: Dedukti, Coq, HRS, CPF.

Added to opam-repository:

Dependencies (16)

  1. ppx_inline_test >= "v0.16.1"
  2. dune-site >= "3.15"
  3. uri >= "1.1"
  4. lwt_ppx >= "1"
  5. yojson >= "1.6"
  6. why3 >= "1.8"
  7. camlp-streams >= "5"
  8. pratter >= "5" & < "6"
  9. timed >= "1"
  10. sedlex >= "3.4"
  11. menhir >= "20200624"
  12. dream >= "1.0.0"
  13. dream-httpaf >= "1.0.0"
  14. dream-pure >= "1.0.0"
  15. ocaml >= "4.14"
  16. dune >= "3.18"

Dev Dependencies (2)

  1. odoc with-doc
  2. alcotest with-test

Optional Dependencies

None

Used by

None

Conflicts

None

Build status

Results of building lambdapi with each compiler on check.ci.ocaml.org, run of against opam-repository 8a77e58. All results for this package.

Each result links to its build log. To keep crawlers from overloading the site, build logs require a GitHub sign-in (see ocurrent/opam-health-check). On your first log, GitHub asks you to “Authorize opam-health-check”, the OCurrent app that runs these checks; it sees only your public profile, not your repositories. The sign-in lasts 30 days.

This version is not in the latest run; the versions below are.

Version OCaml 4.11 OCaml 4.14 OCaml 5.2 OCaml 5.4 OCaml 5.5
3.0.0 good good good good good
  • good Package successfully built
  • partial One of the dependencies failed to build
  • bad Package failed to build
  • n/a Package is not available in this environment
  • internal Internal failure