diff options
| author | pav <pav@FreeBSD.org> | 2004-10-16 00:55:32 +0000 |
|---|---|---|
| committer | pav <pav@FreeBSD.org> | 2004-10-16 00:55:32 +0000 |
| commit | 1acd43444f510aae364a8325c935b699be30b2bc (patch) | |
| tree | f67e449ba94b3220182190280ad8a13df718774b /math/Makefile | |
| parent | 196c9f155c78071ee434ac871e748fcafcd9f6a3 (diff) | |
| download | FreeBSD-ports-1acd43444f510aae364a8325c935b699be30b2bc.zip FreeBSD-ports-1acd43444f510aae364a8325c935b699be30b2bc.tar.gz | |
Add coq, 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".
PR: ports/72718
Submitted by: Rene Ladan <r.c.ladan@student.tue.nl>
Diffstat (limited to 'math/Makefile')
| -rw-r--r-- | math/Makefile | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/math/Makefile b/math/Makefile index 9d64e64..78dafd9 100644 --- a/math/Makefile +++ b/math/Makefile @@ -28,6 +28,7 @@ SUBDIR += cln SUBDIR += concorde SUBDIR += convertall + SUBDIR += coq SUBDIR += cxsc SUBDIR += dcdflib SUBDIR += diehard |
