diff options
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 505587988c..702adc2326 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -56,10 +56,10 @@ sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all products, subsets and function types over these sorts. Formally, we call {\Sort} the set of sorts which is defined by: +\index{Type@{\Type}}% +\index{Prop@{\Prop}}% +\index{Set@{\Set}}% \[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \] -\index{Type@{\Type}} -\index{Prop@{\Prop}} -\index{Set@{\Set}} Their properties are defined in Section~\ref{subtyping-rules}. % TODO: Somewhere in the document we should explain: |