update and shorten description

Author: fblanqui

packages/lambdapi/lambdapi.2.5.1/opam

@@ -1,44 +1,17 @@
 opam-version: "2.0"
 synopsis: "Proof assistant for the λΠ-calculus modulo rewriting"
 description: """
-This package provides:
-- A lambdapi command for checking .lp or .dk files,
-translating .dk files to .lp files and vice versa,
-or launching an LSP server for editing .lp files.
-- A library of logic definitions and basic definitions and proofs
-on natural numbers and polymorphic lists.
-- A rich Emacs mode based on LSP (available on MELPA too).
-- A basic mode for Vim.
-- OCaml libraries.
-A VSCode extension is also available on the VSCode Marketplace.
-
-Find Lambdapi user manual on https://lambdapi.readthedocs.io/.
-
-Lambdapi provides a rich type system with dependent types.
-In Lambdapi, one can define both type and function symbols
-by using rewriting rules (oriented equations).
-A symbol can be declared associative and commutative.
-Lambdapi supports unicode symbols and infix operators.
-The declaration of symbols and rewriting rules is separated
-so that one can easily define inductive-recursive types.
-
-Lambdapi checks that rules are locally confluent (by checking
-the joinability of critical pairs) and preserve typing.
-Rewrite rules can also be exported to the TRS and XTC formats
-for checking confluence and termination with external tools.
-
-Lambdapi does not come with a pre-defined logic. It is a
-powerful logical framework in which one can easily define
-its own logic and build and check proofs in this logic.
-There exist .lp files defining first or higher-order logic
-and complex type systems like in Coq or Agda.
-
-Lambdapi provides a basic module and package system,
-interactive modes for proving both unification goals
-and typing goals, and tactics for solving them step by step.
-In particular, a rewrite tactic like in SSReflect, and
-a why3 tactic for calling external automated provers through
-the Why3 platform."""
+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.
+"""
 maintainer: ["[email protected]"]
 authors: ["Deducteam"]
 license: "CECILL-2.1"