diff options
| author | Tanaka Akira | 2019-02-10 22:57:13 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-02-10 22:57:13 +0900 |
| commit | 4a5eb765f7c1a5795368c7cdcd2a6d85eef20256 (patch) | |
| tree | d9ac1efcc509f675460fec6b4e124946fc7e7d2a | |
| parent | 283046a15dc5e4cd8877df44321dd8020de7bca6 (diff) | |
Change "I" to "I_p".
Since the type of "c" is "I_p ...", the constructor should
return the value of it.
| -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 e227a206d8..38a52c00a3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1663,7 +1663,7 @@ Given a variable :math:`y` of an inductively defined type in a declaration If :math:`c` is :math:`y` or is structurally smaller than :math:`y`, its type is an inductive type :math:`I_p` part of the inductive definition corresponding to :math:`y`. Each :math:`f_i` corresponds to a type of constructor - :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I~p_1 … p_r~t_1 … t_s )` + :math:`C_q ≡ ∀ p_1 :P_1 ,~…,∀ p_r :P_r ,~∀ y_1 :B_1 ,~… ∀ y_m :B_m ,~(I_p~p_1 … p_r~t_1 … t_s )` and can consequently be written :math:`λ y_1 :B_1' .~… λ y_m :B_m'.~g_i`. (:math:`B_i'` is obtained from :math:`B_i` by substituting parameters for variables) the variables :math:`y_j` occurring in :math:`g_i` corresponding to recursive arguments :math:`B_i` (the |