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