diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 37 | ||||
| -rw-r--r-- | doc/sphinx/language/extensions/index.rst | 26 |
2 files changed, 63 insertions, 0 deletions
diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst new file mode 100644 index 0000000000..07dcfff444 --- /dev/null +++ b/doc/sphinx/language/core/index.rst @@ -0,0 +1,37 @@ +.. _core-language: + +============= +Core language +============= + +At the heart of the Coq proof assistant is the Coq kernel. While +users have access to a language with many convenient features such as +notations, implicit arguments, etc. (that are presented in the +:ref:`next chapter <extensions>`), such complex terms get translated +down to a core language (the Calculus of Inductive Constructions) that +the kernel understands, and which we present here. Furthermore, while +users can build proofs interactively using tactics (see Chapter +:ref:`writing-proofs`), the role of these tactics is to incrementally +build a "proof term" which the kernel will verify. More precisely, a +proof term is a term of the Calculus of Inductive Constructions whose +type corresponds to a theorem statement. The kernel is a type checker +which verifies that terms have their expected type. + +This separation between the kernel on the one hand and the elaboration +engine and tactics on the other hand follows what is known as the "de +Bruijn criterion" (keeping a small and well delimited trusted code +base within a proof assistant which can be much more complex). This +separation makes it possible to reduce the trust in the whole system +to trusting a smaller, critical component: the kernel. In particular, +users may rely on external plugins that provide advanced and complex +tactics without fear of these tactics being buggy, because the kernel +will have to check their output. + +.. toctree:: + :maxdepth: 1 + + ../gallina-specification-language + ../cic + ../../addendum/universe-polymorphism + ../../addendum/sprop + ../module-system diff --git a/doc/sphinx/language/extensions/index.rst b/doc/sphinx/language/extensions/index.rst new file mode 100644 index 0000000000..f22927d627 --- /dev/null +++ b/doc/sphinx/language/extensions/index.rst @@ -0,0 +1,26 @@ +.. _extensions: + +=================== +Language extensions +=================== + +Elaboration extends the language accepted by the Coq kernel to make it +easier to use. For example, this lets the user omit most type +annotations because they can be inferred, call functions with implicit +arguments which will be inferred as well, extend the syntax with +notations, factorize branches when pattern-matching, etc. In this +chapter, we present these language extensions and we give some +explanations on how this language is translated down to the core +language presented in the :ref:`previous chapter <core-language>`. + +.. toctree:: + :maxdepth: 1 + + ../gallina-extensions + ../../addendum/extended-pattern-matching + ../../user-extensions/syntax-extensions + ../../addendum/implicit-coercions + ../../addendum/type-classes + ../../addendum/canonical-structures + ../../addendum/program + ../../proof-engine/vernacular-commands |