diff options
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index d3e8755a8..d3b4f3af7 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -59,7 +59,9 @@ Formally, we call {\Sort} the set of sorts which is defined by: \index{Prop@{\Prop}}% \index{Set@{\Set}}% \[\Sort \equiv \{\Prop,\Set,\Type(i)\;|\; i \in \NN\} \] -Their properties are defined in Section~\ref{subtyping-rules}. +Their properties, such as: +{\Prop:\Type$(1)$}, {\Set:\Type$(1)$}, and {\Type$(i)$:\Type$(i+1)$}, +are defined in Section~\ref{subtyping-rules}. % TODO: Somewhere in the document we should explain: % - what concrete actions (in *.v files) cause creation of new universes |