diff options
Diffstat (limited to 'doc/sphinx/language/core/inductive.rst')
| -rw-r--r-- | doc/sphinx/language/core/inductive.rst | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 1642482bb1..d3bd787587 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -17,7 +17,7 @@ Inductive types constructor ::= @ident {* @binder } {? @of_type } This command defines one or more - inductive types and its constructors. |Coq| generates destructors + inductive types and its constructors. Coq generates destructors depending on the universe that the inductive type belongs to. The destructors are named :n:`@ident`\ ``_rect``, :n:`@ident`\ ``_ind``, @@ -411,7 +411,7 @@ constructions. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -552,7 +552,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \end{array} \right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in reset @@ -573,7 +573,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \consf &:& \tree → \forest → \forest\\ \end{array}\right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in @@ -596,7 +596,7 @@ the sort of the inductive type :math:`t` (not to be confused with :math:`\Sort` \oddS &:& ∀ n,~\even~n → \odd~(\nS~n) \end{array}\right]} - which corresponds to the result of the |Coq| declaration: + which corresponds to the result of the Coq declaration: .. coqtop:: in @@ -1099,7 +1099,7 @@ Conversion is preserved as any (partial) instance :math:`I_j~q_1 … q_r` or template polymorphic, even if the :flag:`Auto Template Polymorphism` flag is on. -In practice, the rule **Ind-Family** is used by |Coq| only when all the +In practice, the rule **Ind-Family** is used by Coq only when all the inductive types of the inductive definition are declared with an arity whose sort is in the Type hierarchy. Then, the polymorphism is over the parameters whose type is an arity of sort in the Type hierarchy. @@ -1237,7 +1237,7 @@ at the computational level it implements a generic operator for doing primitive recursion over the structure. But this operator is rather tedious to implement and use. We choose in -this version of |Coq| to factorize the operator for primitive recursion +this version of Coq to factorize the operator for primitive recursion into two more primitive operations as was first suggested by Th. Coquand in :cite:`Coq92`. One is the definition by pattern matching. The second one is a definition by guarded fixpoints. @@ -1252,7 +1252,7 @@ The basic idea of this operator is that we have an object :math:`m` in an inductive type :math:`I` and we want to prove a property which possibly depends on :math:`m`. For this, it is enough to prove the property for :math:`m = (c_i~u_1 … u_{p_i} )` for each constructor of :math:`I`. -The |Coq| term for this proof +The Coq term for this proof will be written: .. math:: @@ -1267,7 +1267,7 @@ Actually, for type checking a :math:`\Match…\with…\kwend` expression we also to know the predicate :math:`P` to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` -(parameters excluded), and the last one corresponds to object :math:`m`. |Coq| +(parameters excluded), and the last one corresponds to object :math:`m`. Coq can sometimes infer this predicate but sometimes not. The concrete syntax for describing this predicate uses the :math:`\as…\In…\return` construction. For instance, let us assume that :math:`I` is an unary predicate |