diff options
| author | Tanaka Akira | 2019-01-31 16:36:26 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 16:36:26 +0900 |
| commit | 6c1c8f1d68ddb11b34411e85f3dc65229f9abe3c (patch) | |
| tree | 7f6540c3b7586ecd284eac3ffb2c9e8243850d3e | |
| parent | d4cc73cb3b8f4ce9d3b8f2cd2e4377989bcbb465 (diff) | |
Use semicolon for separator of local contexts.
| -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 |