diff options
| author | Tanaka Akira | 2019-01-31 15:56:59 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 15:56:59 +0900 |
| commit | dae0b322108d68c7d57837d99a4d15baf6ce5489 (patch) | |
| tree | 246a1ad7914853d6b9f30238ab21e99be75b2565 /doc/sphinx/language | |
| parent | b090f65cf35e45596c10a7513bb3e8058069e4fd (diff) | |
Make "1" and "n" in "u1" and "un" suffixes.
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 6ddfe14eea..5c965527ff 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -84,7 +84,7 @@ implemented using *algebraic universes*. An algebraic universe :math:`u` is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression :math:`u+1`), or an upper bound of algebraic universes (an -expression :math:`\max(u 1 ,...,u n )`), or the base universe (the expression +expression :math:`\max(u_1 ,...,u_n )`), or the base universe (the expression :math:`0`) which corresponds, in the arity of template polymorphic inductive types (see Section :ref:`well-formed-inductive-definitions`), |