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 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). The declaration
20of symbols and rewriting rules is separated so that one can
21easily define inductive-recursive types for instance.
22Rewrite rules can be exported to the TRS and XTC formats
23for checking confluence and termination with external tools.
24A symbol can be declared associative and commutative.
25Lambdapi supports unicode symbols and infix operators.
26
27Lambdapi does not come with a pre-defined logic. It is a
28powerful logical framework in which one can easily define
29its own logic and build and check proofs in this logic.
30There exist .lp files defining first or higher-order logic
31and complex type systems like in Coq or Agda.
32
33Lambdapi provides a basic module and package system,
34interactive modes for proving both unification goals
35and typing goals, and tactics for solving them step by step.
36In particular, a rewrite tactic like in SSReflect, and
37a why3 tactic for calling external automated provers through
38the Why3 platform."""
39maintainer: ["dedukti-dev@inria.fr"]
40authors: ["Deducteam"]
41license: "CECILL-2.1"
42homepage: "https://github.com/Deducteam/lambdapi"
43bug-reports: "https://github.com/Deducteam/lambdapi/issues"
44depends: [
45 "dune" {>= "2.7"}
46 "ocaml" {>= "4.08.0"}
47 "menhir" {>= "20200624"}
48 "sedlex" {>= "2.2"}
49 "alcotest" {with-test}
50 "alt-ergo" {with-test}
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" & <= "1.0.4"}
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.1.0/lambdapi-2.1.0.tbz"
76 checksum: [
77 "sha256=04fac3b56d1855795d7d2d2442bc650183bcd71f676c3ea77f37240e33769ce9"
78 "sha512=37f7bec3bc48632379ca9fb3eb562a0c0387e54afbdd10fb842b8da70c6dad529bb98c14b9d7cddf44a1d5aa61bba86338d310e6a7b420e95b2996b4fbafc95c"
79 ]
80}
81x-commit-hash: "215a0e2434811f026c357f92ca15652e31a945a5"