diff options
| author | Tanaka Akira | 2019-01-25 01:55:05 +0900 |
|---|---|---|
| committer | Tanaka Akira | 2019-01-25 01:55:05 +0900 |
| commit | 03d2931aad83cb7ce7383ee87fa80c108ac33dac (patch) | |
| tree | 142a7937e97c9631691ce771c9a5f28f734ab49f /doc/sphinx/language | |
| parent | 1006fd52c03e7d8ea1d0b612df168f21c9b56455 (diff) | |
Move \def\plus and \def\tri to refman-preamble.sty.
The definition of \plus and \tri in cic.rst is not effective
for HTML output.
So, move them into refman-preamble.sty.
Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 12 |
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: |