From 4a5eb765f7c1a5795368c7cdcd2a6d85eef20256 Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Sun, 10 Feb 2019 22:57:13 +0900
Subject: Change "I" to "I_p".

Since the type of "c" is "I_p ...", the constructor should
return the value of it.
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3