diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b9c17d814..12f390e44 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1120,6 +1120,12 @@ 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 |