From 49bb419465497e302f7ed09d00bdc35b6ec56e62 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 10 Dec 2017 14:17:08 +0100
Subject: [PATCH] Docs: update iris.sty.
Merge it with the JFP paper, we probably need to backport it there.
---
docs/iris.sty | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/docs/iris.sty b/docs/iris.sty
index d55611a86..16c893eaa 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -95,6 +95,9 @@
\newcommand{\nil}{\epsilon}
+% displaced dot
+\newcommand{\dispdot}[2][.2ex]{\dot{\raisebox{0pt}[\dimexpr\height+#1][\depth]{$#2$}}}% \dispdot[<displace>]{<stuff>}
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% MODEL-SPECIFIC SYMBOLS & NOTATION & IDENTIFIERS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -217,6 +220,7 @@
\newcommand{\term}{t}
\newcommand{\termB}{u}
+\newcommand{\venv}{\rho}
\newcommand{\vctx}{\Gamma}
\newcommand{\pfctx}{\Theta}
@@ -242,7 +246,7 @@
\newcommand{\fixp}{\mathit{fix}}
%% various pieces of Syntax
-\def\MU #1.{\mu\spac #1.\spac}%
+\def\MU #1.{\mu #1.\spac}%
\def\Lam #1.{\lambda #1.\spac}%
\newcommand{\proves}{\vdash}
@@ -258,6 +262,8 @@
\NewDocumentCommand\wpre{m O{} m}%
{\textlog{wp}_{#2}\spac#1\spac{\left\{#3\right\}}}
+\newcommand{\stateinterp}{S}
+
\newcommand{\later}{\mathop{{\triangleright}}}
\newcommand*{\lateropt}[1]{\mathop{{\later}^{#1}}}
\newcommand{\always}{\mathop{\Box}}
@@ -291,7 +297,7 @@
}%
}}%
\NewDocumentCommand \vs {O{} O{}} {\vsGen[#1]{\Rrightarrow}[#2]}
-\NewDocumentCommand \bvs {O{} O{}} {\vsGen[#1]{\Rrightarrow_{\mathcal{B}}}[#2]}
+\NewDocumentCommand \bvs {O{} O{}} {\vsGen[#1]{\dispdot[0.02ex]{\Rrightarrow}}[#2]}
\NewDocumentCommand \vsL {O{} O{}} {\vsGen[#1]{\Lleftarrow}[#2]}
\NewDocumentCommand \vsE {O{} O{}} %
{\vsGen[#1]{\Lleftarrow\!\!\!\Rrightarrow}[#2]}
@@ -301,7 +307,7 @@
\NewDocumentCommand \vsW {O{} O{}} {\vsGen[#1]{\vsWand}[#2]}
% for now, the update modality looks like a pvs without masks.
-\NewDocumentCommand \upd {} {\mathop{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}
+\NewDocumentCommand \upd {} {\mathop{\dispdot[-0.2ex]{\mid\kern-0.4ex\Rrightarrow\kern-0.25ex}}}
\NewDocumentCommand\Acc{O{} O{} m m}{\langle #3 \vsE #4 \rangle_{#1}^{#2}}
--
GitLab