freebsd-ports/math/coq/pkg-descr
Pav Lucistnik dc7c8ff64b - Add optional CoqIde support (depends on lablgtk2)
- Correct PORTVERSION to match actual source version
- Cosmetics

PR:		ports/73634
Submitted by:	Rene Ladan <r.c.ladan@student.tue.nl> (maintainer)
2004-11-08 21:57:29 +00:00

23 lines
795 B
Text

From the website:
Developed in the LogiCal project, the Coq tool is a formal proof
management system: a proof done with Coq is mechanically checked
by the machine.
In particular, Coq allows:
* the definition of functions or predicates,
* to state mathematical theorems and software specifications,
* to develop interactively formal proofs of these theorems,
* to check these proofs by a small certification "kernel".
Coq is based on a logical framework called "Calculus of Inductive
Constructions" extended by a modular development system for
theories.
Coq is distributed under the GNU Lesser General Public Licence
Version 2.1 (LGPL).
CoqIde is installed if the x11-toolkits/ocaml-lablgtk2 port is installed.
Author: Rene Ladan <r.c.ladan@student.tue.nl>
WWW: http://coq.inria.fr/