diff options
| -rw-r--r-- | doc/refman/Universes.tex | 23 |
1 files changed, 22 insertions, 1 deletions
diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 2bb1301c79..79b9e4df52 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -139,7 +139,9 @@ producing global universe constraints, one can use the Inductive types, coinductive types, variants and records can be declared cumulative using the \texttt{Cumulative}. Alternatively, there is an option \texttt{Set Inductive Cumulativity} which when set, -makes all subsequent inductive definitions cumulative. Consider the examples below. +makes all subsequent inductive definitions cumulative. When set +inductive types and the like can be enforced to be +\emph{non-cumulative} using the \texttt{NonCumulative} prefix. Consider the examples below. \begin{coq_example*} Polymorphic Cumulative Inductive list {A : Type} := | nil : list @@ -176,6 +178,25 @@ Print packType. \end{coq_example} Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. +Cumulative inductive types, coninductive types, variants and records +only make sense when they are universe polymorphic. Therefore, an +error is issued whenever the user inputs such monomorphic and +cumulative type. Notice that this also implies that when the option +\texttt{Set Inductive Cumulativity} is set any subsequent inductive +declaration should be polymorphic, e.g., by setting \texttt{Set + Universe Polymorphism}, unless it is specifically made +\emph{non-cumulative} using the \texttt{NonCumulative} prefix. + +\begin{coq_example} +Fail Monomorphic Cumulative Inductive Unit := unit. +\end{coq_example} +\begin{coq_example} +Set Inductive Cumulativity. +Fail Inductive Unit := unit. +\end{coq_example} +\begin{coq_example} +NonCumulative Inductive Unit := unit. +\end{coq_example} \asection{Global and local universes} |