Finally, the Vernacular is also used for the management of state: to save theorems, to save proofs, to recall theories from the library.
| Now let us
look into the details of Coq. First of all Coq comes with two languages
-Gallina and the Vernacular. Gallina is the specification language. It is
used to write down actual formulas (in the way of types) and l-terms.
It is a high order l-calculus extended with structured
data types, recursive functions, indicatives predicates and so on. Then
we have the command language, which is called the Vernacular. This is the
language the user exploits to give instructions to the system. We may define
terms, predicates, functions and so on, and interactive proofs are constructed
by giving tactics that are part of the Vernacular. Finally, the Vernacular is also used for the management of state: to save theorems, to save proofs, to recall theories from the library. |
|
