diff options
| author | Tanaka Akira | 2019-01-31 18:00:33 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-31 18:00:33 +0900 |
| commit | 0690df26640cd825f45e62bb10fc6721712bf858 (patch) | |
| tree | 388a90b6c344a8ad326b9a4deba1853440762da6 | |
| parent | cdecb3f5bf0b0302cbfa0374053c97d81426e2c5 (diff) | |
Use \Match for match construct.
| -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 2083eb99a2..4cdc61acc3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1309,7 +1309,7 @@ inference rules, we use a more compact notation: .. _Allowed-elimination-sorts: -**Allowed elimination sorts.** An important question for building the typing rule for match is what +**Allowed elimination sorts.** An important question for building the typing rule for :math:`\Match` is what can be the type of :math:`λ a x . P` with respect to the type of :math:`m`. If :math:`m:I` and :math:`I:A` and :math:`λ a x . P : B` then by :math:`[I:A|B]` we mean that one can use :math:`λ a x . P` with :math:`m` in the above match-construct. |