diff options
Diffstat (limited to 'lang/coq/DESCR')
| -rw-r--r-- | lang/coq/DESCR | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/lang/coq/DESCR b/lang/coq/DESCR new file mode 100644 index 00000000000..43b67beaebc --- /dev/null +++ b/lang/coq/DESCR @@ -0,0 +1,6 @@ +From http://coq.inria.fr/doc/tutorial.html: + + Coq is a Proof Assistant for a Logical Framework known as the + Calculus of Inductive Constructions. It allows the interactive + construction of formal proofs, and also the manipulation of + functional programs consistently with their specifications. |