this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
3description: """
4This package provides:
5- A lambdapi command for checking .lp or .dk files,
6translating .dk files to .lp files and vice versa,
7or launching an LSP server for editing .lp files.
8- A library of logic definitions and basic definitions and proofs
9on natural numbers and polymorphic lists.
10- A rich Emacs mode based on LSP (available on MELPA too).
11- A basic mode for Vim.
12- OCaml libraries.
13A VSCode extension is also available on the VSCode Marketplace.
14
15Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
16
17Lambdapi provides a rich type system with dependent types.
18In Lambdapi, one can define both type and function symbols
19by using rewriting rules (oriented equations).
20A symbol can be declared associative and commutative.
21Lambdapi supports unicode symbols and infix operators.
22The declaration of symbols and rewriting rules is separated
23so that one can easily define inductive-recursive types.
24
25Lambdapi checks that rules are locally confluent (by checking
26the joinability of critical pairs) and preserve typing.
27Rewrite rules can also be exported to the TRS and XTC formats
28for checking confluence and termination with external tools.
29
30Lambdapi does not come with a pre-defined logic. It is a
31powerful logical framework in which one can easily define
32its own logic and build and check proofs in this logic.
33There exist .lp files defining first or higher-order logic
34and complex type systems like in Coq or Agda.
35
36Lambdapi provides a basic module and package system,
37interactive modes for proving both unification goals
38and typing goals, and tactics for solving them step by step.
39In particular, a rewrite tactic like in SSReflect, and
40a why3 tactic for calling external automated provers through
41the Why3 platform."""
42maintainer: ["dedukti-dev@inria.fr"]
43authors: ["Deducteam"]
44license: "CECILL-2.1"
45homepage: "https://github.com/Deducteam/lambdapi"
46bug-reports: "https://github.com/Deducteam/lambdapi/issues"
47depends: [
48 "dune" {>= "2.7"}
49 "ocaml" {>= "4.08.0"}
50 "menhir" {>= "20200624"}
51 "sedlex" {>= "2.2"}
52 "alcotest" {with-test}
53 "alt-ergo" {with-test}
54 "bindlib" {>= "5.0.1"}
55 "timed" {>= "1.0"}
56 "pratter" {>= "1.2" & < "2.0.0"}
57 "why3" {>= "1.4" & < "1.5~"}
58 "yojson" {>= "1.6.0"}
59 "cmdliner" {>= "1.1.0"}
60 "stdlib-shims" {>= "0.1.0"}
61 "odoc" {with-doc}
62]
63build: [
64 ["dune" "subst"] {dev}
65 [
66 "dune"
67 "build"
68 "-p"
69 name
70 "-j"
71 jobs
72 "@install"
73 ]
74]
75dev-repo: "git+https://github.com/Deducteam/lambdapi.git"
76url {
77 src:
78 "https://github.com/Deducteam/lambdapi/releases/download/2.2.0/lambdapi-2.2.0.tbz"
79 checksum: [
80 "sha256=920de48ec6c2c3223b6b93879bb65d07ea24aa27f7f7176b3de16e5e467b9939"
81 "sha512=135f132730825adeb084669222e68bc999de97b12378fae6abcd9f91ae13093eab29fa49c854adb28d064d52c9890c0f5c8ff9d47a9916f66fe5e0fba3479759"
82 ]
83}
84x-commit-hash: "0476fbec66e99750abe9d60c3aa9cb9a52189bea"