diff options
| author | Matej Kosik | 2015-10-29 10:27:51 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-10 09:35:08 +0100 |
| commit | 05276561ebff16d434b475b9e80586194619a832 (patch) | |
| tree | f3008641f84db3968bfc566e165d09c105ae1892 | |
| parent | 950dace27c3233f740b2031c9d99cb3f155aefbf (diff) | |
ENH: the concept of the 'algebraic universe' was added to the 'Global Index'.
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 702adc2326..7f9d4e5ecb 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -78,8 +78,9 @@ We shall make precise in the typing rules the constraints between the indexes. \paragraph{Implementation issues} -In practice, the {\Type} hierarchy is implemented using algebraic -universes. An algebraic universe $u$ is either a variable (a qualified +In practice, the {\Type} hierarchy is implemented using +{\em algebraic universes}\index{algebraic universe}. +An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression |