diff options
author | 2015-11-03 10:45:04 +0100 | |
---|---|---|
committer | 2015-12-10 09:35:12 +0100 | |
commit | 4570133034c9457a4d641449a522c29a8f029a55 (patch) | |
tree | 7fd5ccff4ea649f02ce1449422ad380744e56333 /doc/refman/RefMan-cic.tex | |
parent | 6c9f5450f476da94aa70df93c5a6368b98e73e90 (diff) |
FIX: commit 315f771
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 |