diff options
author | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-03-31 15:03:34 +0200 |
---|---|---|
committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-11 12:50:26 +0200 |
commit | d3a2acc9fceff7476bc2d9eaadab8411365172a2 (patch) | |
tree | c52f4bcda00aa77444d8a92c23ccc6e78a2ddf9e /doc | |
parent | 41b3486501f0217f0b0c552f21d6f0374b55a3ba (diff) |
Use "template polymorphism" in the documentation.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-cic.tex | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 12f390e44..e26d4b18d 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression -$0$) which corresponds, in the arity of sort-polymorphic inductive -types (see Section \ref{Sort-polymorphism-inductive}), +$0$) which corresponds, in the arity of template polymorphic inductive +types (see Section \ref{Template-polymorphism}), to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of @@ -977,8 +977,8 @@ 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 types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}} -\label{Sort-polymorphism-inductive} +\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} +\label{Template-polymorphism} Inductive types declared in {\Type} are polymorphic over their arguments in {\Type}. @@ -1120,12 +1120,6 @@ Check (fun (A:Prop) (B:Set) => prod A B). Check (fun (A:Type) (B:Prop) => prod A B). \end{coq_example} -Internally, Coq calls sort polymorphism of inductive types -{\em template polymorphism}. For instance: -\begin{coq_example} -About prod. -\end{coq_example} - \subsection{Destructors} The specification of inductive definitions with arities and constructors is quite natural. But we still have to say how to use an |