diff options
Diffstat (limited to 'doc/sphinx/language/core')
| -rw-r--r-- | doc/sphinx/language/core/coinductive.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/definitions.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/core/index.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/core/modules.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/language/core/sorts.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/language/core/variants.rst | 6 |
7 files changed, 56 insertions, 14 deletions
diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 51860aec0d..c034b7f302 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -14,6 +14,9 @@ constructors. Infinite objects are introduced by a non-ending (but effective) process of construction, defined in terms of the constructors of the type. +More information on co-inductive definitions can be found in +:cite:`Gimenez95b,Gim98,GimCas05`. + .. cmd:: CoInductive @inductive_definition {* with @inductive_definition } This command introduces a co-inductive type. diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 679022a5b1..0e637e5aa3 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -72,11 +72,12 @@ Section :ref:`typing-rules`. .. cmd:: {| Definition | Example } @ident_decl @def_body :name: Definition; Example - .. insertprodn def_body def_body + .. insertprodn def_body reduce .. prodn:: def_body ::= {* @binder } {? : @type } := {? @reduce } @term | {* @binder } : @type + reduce ::= Eval @red_expr in These commands bind :n:`@term` to the name :n:`@ident` in the environment, provided that :n:`@term` is well-typed. They can take the :attr:`local` :term:`attribute`, diff --git a/doc/sphinx/language/core/index.rst b/doc/sphinx/language/core/index.rst index 5e83672463..de780db267 100644 --- a/doc/sphinx/language/core/index.rst +++ b/doc/sphinx/language/core/index.rst @@ -34,10 +34,17 @@ will have to check their output. :maxdepth: 1 basic - ../gallina-specification-language + sorts + assumptions + definitions + conversion ../cic + variants records + inductive + coinductive + sections + modules + primitive ../../addendum/universe-polymorphism ../../addendum/sprop - sections - ../module-system diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 189e1008e8..53c8cd4701 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -333,10 +333,6 @@ Mutually defined inductive types A generic command :cmd:`Scheme` is useful to build automatically various mutual induction principles. -.. [1] - Except if the inductive type is empty in which case there is no - equation that can be used to infer the return type. - .. index:: single: fix @@ -548,7 +544,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` which corresponds to the result of the |Coq| declaration: - .. coqtop:: in + .. coqtop:: in reset Inductive list (A:Set) : Set := | nil : list A @@ -1103,7 +1099,7 @@ respect to the hierarchy :math:`\Prop ⊂ \Set_p ⊂ \Type` where :math:`\Set_p` (i.e. an inductive definition of which all inductive types are singleton – see Section :ref:`Destructors`) is set in :math:`\Prop`, a small non-singleton inductive type is set in :math:`\Set` (even in case :math:`\Set` is impredicative – see -Section The-Calculus-of-Inductive-Construction-with-impredicative-Set_), +:ref:`The-Calculus-of-Inductive-Construction-with-impredicative-Set`), and otherwise in the Type hierarchy. Note that the side-condition about allowed elimination sorts in the rule diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 74977e7088..b06dd2f1ab 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -864,7 +864,7 @@ The theories developed in |Coq| are stored in *library files* which are hierarchically classified into *libraries* and *sublibraries*. To express this hierarchy, library names are represented by qualified identifiers qualid, i.e. as list of identifiers separated by dots (see -:ref:`gallina-identifiers`). For instance, the library file ``Mult`` of the standard +:ref:`qualified-names`). For instance, the library file ``Mult`` of the standard |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts the name of a library is called a *library root*. All library files of the standard library of |Coq| have the reserved root |Coq| but library @@ -875,8 +875,14 @@ started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-opt .. _qualified-names: -Qualified names -~~~~~~~~~~~~~~~ +Qualified identifiers +--------------------- + +.. insertprodn qualid field_ident + +.. prodn:: + qualid ::= @ident {* @field_ident } + field_ident ::= .@ident Library files are modules which possibly contain submodules which eventually contain constructions (axioms, parameters, definitions, diff --git a/doc/sphinx/language/core/sorts.rst b/doc/sphinx/language/core/sorts.rst index 3fa5f826df..8307a02d6d 100644 --- a/doc/sphinx/language/core/sorts.rst +++ b/doc/sphinx/language/core/sorts.rst @@ -1,8 +1,27 @@ -.. _Sorts: +.. index:: + single: Set (sort) + single: SProp + single: Prop + single: Type + +.. _sorts: Sorts ~~~~~~~~~~~ +.. insertprodn sort universe_expr + +.. prodn:: + sort ::= Set + | Prop + | SProp + | Type + | Type @%{ _ %} + | Type @%{ @universe %} + universe ::= max ( {+, @universe_expr } ) + | @universe_expr + universe_expr ::= @universe_name {? + @num } + The types of types are called :gdef:`sort`\s. All sorts have a type and there is an infinite well-founded typing @@ -13,6 +32,8 @@ The sort :math:`\Prop` intends to be the type of logical propositions. If :math: logical proposition then it denotes the class of terms representing proofs of :math:`M`. An object :math:`m` belonging to :math:`M` witnesses the fact that :math:`M` is provable. An object of type :math:`\Prop` is called a proposition. +We denote propositions by :n:`@form`. +This constitutes a semantic subclass of the syntactic class :n:`@term`. The sort :math:`\SProp` is like :math:`\Prop` but the propositions in :math:`\SProp` are known to have irrelevant proofs (all proofs are @@ -24,6 +45,8 @@ considerations. The sort :math:`\Set` intends to be the type of small sets. This includes data types such as booleans and naturals, but also products, subsets, and function types over these data types. +We denote specifications (program types) by :n:`@specif`. +This constitutes a semantic subclass of the syntactic class :n:`@term`. :math:`\SProp`, :math:`\Prop` and :math:`\Set` themselves can be manipulated as ordinary terms. Consequently they also have a type. Because assuming simply that :math:`\Set` diff --git a/doc/sphinx/language/core/variants.rst b/doc/sphinx/language/core/variants.rst index 315e97687b..6d4676b3c4 100644 --- a/doc/sphinx/language/core/variants.rst +++ b/doc/sphinx/language/core/variants.rst @@ -52,6 +52,8 @@ Private (matching) inductive types .. index:: match ... with ... +.. _match: + Definition by cases: match -------------------------- @@ -194,3 +196,7 @@ a type with annotations. For this third subcase, both the clauses ``as`` and There are specific notations for case analysis on types with one or two constructors: ``if … then … else …`` and ``let (…,…) := … in …`` (see Sections :ref:`if-then-else` and :ref:`irrefutable-patterns`). + +.. [1] + Except if the inductive type is empty in which case there is no + equation that can be used to infer the return type. |