diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/newfaq/main.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 08123b7da..2277fc3f8 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -1161,6 +1161,8 @@ You can provide programs for your axioms. \Question{Can you explain me what an evaluable constant is ?} +An evaluable constant is a constant which is unfoldable. + \Question{What is a goal ?} The goal is the statement to be proved. @@ -1170,14 +1172,14 @@ The goal is the statement to be proved. A meta variable in \Coq represents a ``hole'', i.e. a part of a proof that is still unknown. -\Question{What is a constr ?} - \Question{What is Gallina ?} Gallina is the specification language of \Coq. Complete documentation of this language can be found in the Reference Manual. -\Question{What is a command ?} +\Question{What is The Vernacular ?} + +It is the language of commands of Gallina i.e. definitions, lemmas, \ldots \Question{What is a dependent type ?} |