···
2
+
synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
4
+
Lambdapi is an interactive proof assistant for the λΠ-calculus modulo
5
+
rewriting. It can call external automated theorem provers via Why3.
6
+
The user manual is on https://lambdapi.readthedocs.io/.
7
+
A standard library and other developments are available on
8
+
https://github.com/Deducteam/opam-lambdapi-repository/. An extension
9
+
for Emacs is available on MELPA. An extension for VSCode is available
10
+
on the VSCode Marketplace. Lambdapi can read Dedukti files. It
11
+
includes checkers for local confluence and subject reduction. It also
12
+
provides commands to export Lambdapi files to other formats or
13
+
systems: Dedukti, Coq, HRS, CPF.
15
+
maintainer: ["dedukti-dev@inria.fr"]
16
+
authors: ["Deducteam"]
17
+
license: "CECILL-2.1"
18
+
homepage: "https://github.com/Deducteam/lambdapi"
19
+
bug-reports: "https://github.com/Deducteam/lambdapi/issues"
20
+
dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
23
+
"ocaml" {>= "4.08.0"}
24
+
"menhir" {>= "20200624"}
26
+
"alcotest" {with-test}
27
+
"dedukti" {with-test & >= "2.7"}
28
+
"bindlib" {>= "6.0.0"}
30
+
"pratter" {>= "3.0.0" & < "4"}
31
+
"camlp-streams" {>= "5.0"}
32
+
"why3" {>= "1.6.0" & < "1.8~"}
33
+
"yojson" {>= "1.6.0"}
34
+
"cmdliner" {>= "1.1.0"}
35
+
"stdlib-shims" {>= "0.1.0"}
37
+
"lwt_ppx" {>= "1.0.0"}
38
+
"dream" {>= "1.0.0~alpha3"}
41
+
["dune" "subst"] {dev}
50
+
"@runtest" {with-test}
54
+
conflicts: [ "ocaml-option-bytecode-only" ]
57
+
"https://github.com/Deducteam/lambdapi/releases/download/2.5.1/lambdapi-2.5.1.tbz"
59
+
"sha256=2c251021b6fac40c05282ca183902da5b1008e69d9179d7a9543905c2c21a28a"
60
+
"sha512=69535f92766e6fedc2675fc214f0fb699bde2a06aa91d338c93c99756235a293cf16776f6328973dda07cf2ad402e58fe3104a08f1a896990c1778b42f7f9fcf"
63
+
x-commit-hash: "e119c8cee3647e1d17fa6fdaf1bb6129f42927bc"