aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/common
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2015-11-03 16:59:08 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 09:35:14 +0100
commitc5a7d2bec3232625dcb50cfc3a3d6d5abcb81ff0 (patch)
tree48c2f4435be8857b0ccb1f7def53afab2288867f /doc/common
parent5a155b13b6a6820a1c0417025c67170a3e22fedc (diff)
ENH: examples for 'strict positivity' were expanded
Diffstat (limited to 'doc/common')
-rw-r--r--doc/common/macros.tex4
1 files changed, 3 insertions, 1 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 2271a8f13..3b12f259b 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -261,7 +261,7 @@
\newcommand{\length}{\mbox{\textsf{length}}}
\newcommand{\haslengthA}{\mbox {\textsf{has\_length~A}}}
\newcommand{\List}{\mbox{\textsf{list}}}
-\newcommand{\ListA}{\mbox{\textsf{List}~A}}
+\newcommand{\ListA}{\mbox{\textsf{list}}~\ensuremath{A}}
\newcommand{\nilhl}{\mbox{\textsf{nil\_hl}}}
\newcommand{\conshl}{\mbox{\textsf{cons\_hl}}}
\newcommand{\nat}{\mbox{\textsf{nat}}}
@@ -285,6 +285,8 @@
\newcommand{\evenO}{\mbox{\textsf{even\_O}}}
\newcommand{\evenS}{\mbox{\textsf{even\_S}}}
\newcommand{\oddS}{\mbox{\textsf{odd\_S}}}
+\newcommand{\Prod}{\mbox{\textsf{prod}}}
+\newcommand{\Pair}{\mbox{\textsf{pair}}}
%%%%%%%%%
% Misc. %