diff options
| author | Matej Kosik | 2015-11-03 10:45:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:12 +0100 |
| commit | 4570133034c9457a4d641449a522c29a8f029a55 (patch) | |
| tree | 7fd5ccff4ea649f02ce1449422ad380744e56333 | |
| parent | 6c9f5450f476da94aa70df93c5a6368b98e73e90 (diff) | |
FIX: commit 315f771
| -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 d3e8755a85..d3b4f3af7c 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 |