diff options
| author | pav <pav@FreeBSD.org> | 2004-10-16 08:55:32 +0800 |
|---|---|---|
| committer | pav <pav@FreeBSD.org> | 2004-10-16 08:55:32 +0800 |
| commit | 1acd43444f510aae364a8325c935b699be30b2bc (patch) | |
| tree | f67e449ba94b3220182190280ad8a13df718774b /textproc/tex2im/Makefile | |
| parent | 196c9f155c78071ee434ac871e748fcafcd9f6a3 (diff) | |
| download | freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.tar.gz freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.tar.zst freebsd-ports-gnome-1acd43444f510aae364a8325c935b699be30b2bc.zip | |
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 'textproc/tex2im/Makefile')
0 files changed, 0 insertions, 0 deletions