diff options
| author | Joachim Breitner | 2018-09-16 21:33:13 +0200 |
|---|---|---|
| committer | Joachim Breitner | 2018-09-16 21:33:13 +0200 |
| commit | 69e852924a9419eeff5cf5875f649fd898d2ba07 (patch) | |
| tree | 9508be59c3e77997db149e88839f33add330b031 | |
| parent | 8dff82ee590de2f6f55918d2bbf2a3d0f9a54e65 (diff) | |
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 |