diff options
| author | Timothy Bourke | 2018-07-22 07:43:32 +0200 |
|---|---|---|
| committer | Timothy Bourke | 2018-07-22 07:43:32 +0200 |
| commit | f25c1d252ad61b4dc4321e3a11f33b1e6d4e3dff (patch) | |
| tree | b4ae4c93262942f8ca825052e036849c9bb73af6 | |
| parent | 6bce3de10ec1cd18c60e1ce3b5af33350ec4ac86 (diff) | |
Docs: minor typo in W-Ind relative to text
The rule uses s'_j, the text refers to s_j, the latter is simpler in the
absence of any other constraints.
| -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 9f932ae78f..b670305389 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -961,7 +961,7 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;…;I_k :∀ Γ_P ,A_k]`, .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j' )_{j=1… k} + (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ \WF{E;\ind{p}{Γ_I}{Γ_C}}{Γ} |