diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index cd366e424b..030214fe46 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1598,7 +1598,7 @@ The typing rule is the expected one for a fixpoint. .. inference:: Fix (E[Γ] ⊢ A_i : s_i )_{i=1… n} - (E[Γ,f_1 :A_1 ,…,f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} + (E[Γ;f_1 :A_1 ;…;f_n :A_n ] ⊢ t_i : A_i )_{i=1… n} ------------------------------------------------------- E[Γ] ⊢ \Fix~f_i\{f_1 :A_1 :=t_1 … f_n :A_n :=t_n \} : A_i @@ -1776,8 +1776,8 @@ and :math:`\subst{E}{|Γ|}{|Γ|c}` to mean the parallel substitution .. math:: \frac{\WF{E;c:U;E′;\ind{p}{Γ_I}{Γ_C};E″}{Γ}} {\WFTWOLINES{E;c:U;E′;\ind{p+1}{∀ x:U,~\subst{Γ_I}{c}{x}}{∀ x:U,~\subst{Γ_C}{c}{x}}; - \subst{E″}{|Γ_I ,Γ_C |}{|Γ_I ,Γ_C | c}} - {\subst{Γ}{|Γ_I ,Γ_C|}{|Γ_I ,Γ_C | c}}} + \subst{E″}{|Γ_I ;Γ_C |}{|Γ_I ;Γ_C | c}} + {\subst{Γ}{|Γ_I ;Γ_C|}{|Γ_I ;Γ_C | c}}} One can similarly modify a global declaration by generalizing it over a previously defined constant :math:`c′`. Below, if :math:`Γ` is a context of the form |