diff options
| author | Théo Zimmermann | 2019-02-20 16:19:25 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-20 16:19:25 +0100 |
| commit | 27838d59f12fde650191c61f3d2168daa1ac2bd3 (patch) | |
| tree | 761133fddc362a4adf28b8b1bc0560be441c939a | |
| parent | 756b978dfee0e0c103a5244af21115233ad96358 (diff) | |
| parent | 6031ab6f20bc2fb160ce5a47ab34f34c6cd25e5e (diff) | |
Merge PR #9457: Correct W-Ind in Cic description of the reference manual.
Reviewed-by: SkySkimmer
| -rw-r--r-- | doc/sphinx/language/cic.rst | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 3ef88e6506..e05df65c63 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -963,10 +963,9 @@ 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[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} provided that the following side conditions hold: @@ -976,7 +975,7 @@ provided that the following side conditions hold: context of parameters, + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`, + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which - satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`. + satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ E`. One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its |