diff options
| author | Tanaka Akira | 2019-01-31 16:37:59 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:37:59 +0900 |
| commit | ad13db81f25f48d1a0c800b16200426003c08b07 (patch) | |
| tree | 8b2c5effd529e4ebc745168285a0f723cbc8ec95 /doc | |
| parent | 6c1c8f1d68ddb11b34411e85f3dc65229f9abe3c (diff) | |
\Sort is not a term.
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort" is changed to
"∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S" because
\Sort is not a term.
"S" is choosen to be consistent with the description of
Inductive Definitions.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 030214fe46..d63adf218d 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -618,9 +618,9 @@ a *subtyping* relation inductively defined by: #. if :math:`\ind{p}{Γ_I}{Γ_C}` is a universe polymorphic and cumulative (see Chapter :ref:`polymorphicuniverses`) inductive type (see below) and - :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, \Sort)∈Γ_I` + :math:`(t : ∀Γ_P ,∀Γ_{\mathit{Arr}(t)}, S)∈Γ_I` and - :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', \Sort')∈Γ_I` + :math:`(t' : ∀Γ_P' ,∀Γ_{\mathit{Arr}(t)}', S')∈Γ_I` are two different instances of *the same* inductive type (differing only in universe levels) with constructors |