diff options
Diffstat (limited to 'doc/sphinx')
| -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 35f45e2e0e..ac0f0f8ea6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -605,7 +605,7 @@ Subtyping rules At the moment, we did not take into account one rule between universes which says that any term in a universe of index i is also a term in -the universe of index i+1 (this is the *cumulativity* rule of|Cic|). +the universe of index i+1 (this is the *cumulativity* rule of |Cic|). This property extends the equivalence relation of convertibility into a *subtyping* relation inductively defined by: @@ -640,7 +640,7 @@ a *subtyping* relation inductively defined by: respectively then .. math:: - E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t~w_1' … w_m' + E[Γ] ⊢ t~w_1 … w_m ≤_{βδιζη} t'~w_1' … w_m' (notice that :math:`t` and :math:`t'` are both fully applied, i.e., they have a sort as a type) if |