aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorTanaka Akira2019-02-08 14:03:59 +0900
committerTanaka Akira2019-02-08 14:03:59 +0900
commit3b79feaf661e8ebe6092849c9d30a5276366c01e (patch)
tree8b0408d8aec91d929d753af197c90c0743abe6ce /kernel
parent7532f36176c2644bd9167c95fcd33ef3eff631af (diff)
Change parameters p_1...p_r to q_1...q_r.
In the description of destructors, "Type of branches" section and "Typing rule" section shares the definition of "r" (and "s" from previous commit). However actual parameters are p_1...p_r in the former section and q_1...q_r in the latter section. I guess it's because the latter section uses p_1...p_l in other purpose: index of constructor for a inductive type. So, I change the parameter p_1...p_r to q_1...q_r in the former section to consistent with the latter section.
Diffstat (limited to 'kernel')
0 files changed, 0 insertions, 0 deletions