aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/language
diff options
context:
space:
mode:
Diffstat (limited to 'doc/sphinx/language')
-rw-r--r--doc/sphinx/language/cic.rst12
1 files changed, 5 insertions, 7 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst
index 91504089a8..25a230015c 100644
--- a/doc/sphinx/language/cic.rst
+++ b/doc/sphinx/language/cic.rst
@@ -1719,13 +1719,11 @@ possible:
.. math::
:nowrap:
- {\def\plus{\mathsf{plus}}
- \def\tri{\triangleright_\iota}
- \begin{eqnarray*}
- \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
- & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
- & \tri & \nS~(\nS~(\nS~\nO))\\
- \end{eqnarray*}}
+ \begin{eqnarray*}
+ \plus~(\nS~(\nS~\nO))~(\nS~\nO)~& \trii & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\
+ & \trii & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\
+ & \trii & \nS~(\nS~(\nS~\nO))\\
+ \end{eqnarray*}
.. _Mutual-induction: