2011-08-05 22:11:34 +08:00
|
|
|
Coq implements a program specification and mathematical higher-level
|
|
|
|
|
language called Gallina that is based on an expressive formal language
|
|
|
|
|
called the Calculus of Inductive Constructions that itself combines both
|
|
|
|
|
a higher-order logic and a richly-typed functional programming language.
|
|
|
|
|
|
2012-08-22 09:28:50 +08:00
|
|
|
If you have ocamlopt, Coq will be compiled to native code, which runs 4-10
|
|
|
|
|
times faster. For best performance, OCaml should have support for pthreads.
|
2011-08-05 22:11:34 +08:00
|
|
|
|
|
|
|
|
If you want CoqIDE, you need LablGTK2 (>= 2.10.0) with development
|
|
|
|
|
files, and GTK2+ (>= 2.10.0). This also REQUIRES OCaml to have support
|
|
|
|
|
for pthreads.
|
|
|
|
|
|
|
|
|
|
If you have emacs installed, emacs files for Coq will be installed.
|
|
|
|
|
Otherwise, they will be omitted.
|
