diff options
| author | Théo Zimmermann | 2019-01-28 14:17:06 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-28 14:17:06 +0100 |
| commit | 9d9bc6fa0eb3d83218f7ed025cacab4875e555ea (patch) | |
| tree | 4087f9476f0884255611e72baa39cf8377a8771d | |
| parent | 562a731fd380be3e3ba8318348a9b92ca6cc1668 (diff) | |
| parent | 03d2931aad83cb7ce7383ee87fa80c108ac33dac (diff) | |
Merge PR #9402: Move \def\plus and \def\tri to refman-preamble.sty.
Reviewed-by: Zimmi48
| -rw-r--r-- | doc/sphinx/language/cic.rst | 12 | ||||
| -rw-r--r-- | doc/sphinx/refman-preamble.sty | 2 |
2 files changed, 7 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: diff --git a/doc/sphinx/refman-preamble.sty b/doc/sphinx/refman-preamble.sty index b4fc608e47..cb7c8d0cf5 100644 --- a/doc/sphinx/refman-preamble.sty +++ b/doc/sphinx/refman-preamble.sty @@ -56,6 +56,7 @@ \newcommand{\oddS}{\textsf{odd}_\textsf{S}} \newcommand{\ovl}[1]{\overline{#1}} \newcommand{\Pair}{\textsf{pair}} +\newcommand{\plus}{\mathsf{plus}} \newcommand{\Prod}{\textsf{prod}} \newcommand{\Prop}{\textsf{Prop}} \newcommand{\return}{\kw{return}} @@ -68,6 +69,7 @@ \newcommand{\subst}[3]{#1\{#2/#3\}} \newcommand{\tl}{\textsf{tl}} \newcommand{\tree}{\textsf{tree}} +\newcommand{\trii}{\triangleright_\iota} \newcommand{\true}{\textsf{true}} \newcommand{\Type}{\textsf{Type}} \newcommand{\unfold}{\textsf{unfold}} |