From 3062110eca5ea6f190d10b07716ee20b9bc2b6ad Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 8 Feb 2019 17:03:37 +0900
Subject: Fix index of arguments of constructor in fixpoint.

In fixpoint typing rule section, a type of constructor is described
twice:

- ∀ p_1:P_1,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r:T_r,~(I_j~p_1 … p_r~t_1 … t_s)
- ∀ p_1:P_1,~…,∀ p_r :P_r,~∀ y_1:B_1,~… ∀ y_k:B_k,~(I~a_1 … a_k)

Both seems invalid.
The former require that the number of parameters and
the number of (non-parameter) constructor argumets is same.
The latter require that the number of (non-parameter) constructor
argumets and the number of inductive type arguments (including paramters) is
same.
Also, "k" is already used for the number of inductive types in
a inductive definition.

So, I changed the number of (non-parameter) constructor
argumets to "m".  I choose "m" because "m" is used for the purpose
in the description for iota-reduction of destructors.

Also, I changed the inductive type parameters and arguments of latter
consistent with the former.
---
 doc/sphinx/language/cic.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index a3fa12c618..1d3076d90e 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1648,7 +1648,7 @@ The definition of being structurally smaller is a bit technical. One
 needs first to define the notion of *recursive arguments of a
 constructor*. For an inductive definition :math:`\ind{r}{Γ_I}{Γ_C}`, if the
 type of a constructor :math:`c` has the form
-:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_r :T_r,~(I_j~p_1 … p_r~t_1 … t_s )`,
+:math:`∀ p_1 :P_1 ,~… ∀ p_r :P_r,~∀ x_1:T_1,~… ∀ x_m :T_m,~(I_j~p_1 … p_r~t_1 … t_s )`,
 then the recursive
 arguments will correspond to :math:`T_i` in which one of the :math:`I_l` occurs.
 
@@ -1663,8 +1663,8 @@ 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
   definition :math:`I_p` part of the inductive declaration 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_k :B_k ,~(I~a_1 … a_k )`
-  and can consequently be written :math:`λ y_1 :B_1' .~… λ y_k :B_k'.~g_i`. (:math:`B_i'` is
+  :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 )`
+  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
   ones in which one of the :math:`I_l` occurs) are structurally smaller than y.
-- 
cgit v1.2.3