diff options
| author | Tanaka Akira | 2019-01-31 19:00:55 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 19:00:55 +0900 |
| commit | fcb4cf7628ea67cf342f8c39cb7f5151897ff72c (patch) | |
| tree | d549d1e2ff7bb2b900794433036b228dca8959aa | |
| parent | 382bd13a0cb7a045eef93db25e4fc45d7214c839 (diff) | |
Use "U" instead of "u" for a type.
| -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 2c8074be69..e3fd543c93 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1658,7 +1658,7 @@ Given a variable :math:`y` of an inductively defined type in a declaration :math:`[c_1 :C_1 ;~…;~c_n :C_n ]`, the terms structurally smaller than :math:`y` are: -+ :math:`(t~u)` and :math:`λ x:u .~t` when :math:`t` is structurally smaller than :math:`y`. ++ :math:`(t~u)` and :math:`λ x:U .~t` when :math:`t` is structurally smaller than :math:`y`. + :math:`\case(c,P,f_1 … f_n)` when each :math:`f_i` is structurally smaller than :math:`y`. 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`. |