diff options
| author | Théo Zimmermann | 2018-09-18 09:55:27 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2018-09-18 09:55:27 +0200 |
| commit | 15649c16bc4e20ef2c2b1b0ac645f83ee03c3589 (patch) | |
| tree | ea6cbdc24545b971ff8a3b374f234609e811de6a | |
| parent | 11aa55dc20c7311229d55e17d7356cff8a4b4bbc (diff) | |
| parent | 69e852924a9419eeff5cf5875f649fd898d2ba07 (diff) | |
Merge PR #8486: Mising prime in the subtyping rules
| -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 9c2ba50362..ac0f0f8ea6 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -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 |