diff options
| author | Hugo Herbelin | 2015-10-06 19:49:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:06 +0100 |
| commit | 19a3cb9cf627e593026a675ff7201bb1dc8e3574 (patch) | |
| tree | 3895b0409d6667b3371c95c3cc252c7981cb3d57 | |
| parent | ba00ffda884142fdd1b4d8b0888d3c9a35457c99 (diff) | |
RefMan, ch. 4: Avoiding using "inductive family" which is not defined.
Using consistently "inductive types".
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index aa4483759e..174f318fed 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -631,7 +631,7 @@ the value over the parameter. In the case of inductive definitions we have to handle the abstraction over several objects. One possible way to do that would be to define the type \List\ -inductively as being an inductive family of type $\Set\ra\Set$: +inductively as being an inductive type of type $\Set\ra\Set$: \[\NInd{}{\List:\Set\ra\Set}{\Nil:(\forall A:\Set,\List~A), \cons : (\forall A:\Set, A \ra \List~A \ra \List~A)}\] There are drawbacks to this point of view. The @@ -961,10 +961,10 @@ Inductive exType (P:Type->Prop) : Type %is recursive or not. We shall write the type $(x:_R T)C$ if it is %a recursive argument and $(x:_P T)C$ if the argument is not recursive. -\paragraph[Sort-polymorphism of inductive families.]{Sort-polymorphism of inductive families.\index{Sort-polymorphism of inductive families}} +\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}} \label{Sort-polymorphism-inductive} -From {\Coq} version 8.1, inductive families declared in {\Type} are +From {\Coq} version 8.1, inductive types declared in {\Type} are polymorphic over their arguments in {\Type}. If $A$ is an arity of some sort and $s$ is a sort, we write $A_{/s}$ for the arity @@ -1057,7 +1057,7 @@ predicative {\Set}. More precisely, an empty or small singleton inductive definition (i.e. an inductive definition of which all inductive types are singleton -- see paragraph~\ref{singleton}) is set in -{\Prop}, a small non-singleton inductive family is set in {\Set} (even +{\Prop}, a small non-singleton inductive type is set in {\Set} (even in case {\Set} is impredicative -- see Section~\ref{impredicativity}), and otherwise in the {\Type} hierarchy. % TODO: clarify the case of a partial application ?? |