From c37310668a0aa817c2bb9823a373c0fc26d4ff65 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 31 Oct 2016 11:26:02 +0100
Subject: [PATCH] update iris.sty
---
docs/iris.sty | 12 ++++++++----
docs/program-logic.tex | 2 +-
2 files changed, 9 insertions(+), 5 deletions(-)
diff --git a/docs/iris.sty b/docs/iris.sty
index 8999ed4bd..9c5becfcd 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -78,15 +78,19 @@
\newcommand{\pset}[1]{\wp(#1)} % Powerset
\newcommand{\psetdown}[1]{\wp^\downarrow(#1)}
\newcommand{\finpset}[1]{\wp^\mathrm{fin}(#1)}
+\newcommand{\pmultiset}[1]{\wp^{+}(#1)}
+\newcommand{\finpmultiset}[1]{\wp^{\mathrm{fin},+}(#1)}
\newcommand{\Func}{F} % functor
\newcommand{\subst}[3]{{#1}[{#3} / {#2}]}
-\newcommand{\mapinsert}[3]{#3[#1\mathop{\vcentcolon=}#2]}
-\newcommand{\mapsingleton}[2]{[#1\mathop{\vcentcolon=}#2]}
-\newcommand{\mapsingletonComp}[3]
- {\left[ #1 \mathop{\vcentcolon=} #2 \spac\middle|\spac #3 \right]}
+\newcommand{\mapinsert}[3]{#3\left[#1\mathop{\la}#2\right]}
+\newcommand{\mapsingleton}[2]{\mapinsert{#1}{#2}{}}
+\newcommand{\mapinsertComp}[4]
+ {\mapinsert{#1}{#2 \spac\middle|\spac #3}{#4}}
+\newcommand{\mapComp}[3]
+ {\mapinsertComp{#1}{#2}{#3}{}}
\newcommand{\nil}{\epsilon}
diff --git a/docs/program-logic.tex b/docs/program-logic.tex
index c4f3bb15d..c3c8be440 100644
--- a/docs/program-logic.tex
+++ b/docs/program-logic.tex
@@ -130,7 +130,7 @@ We can now define the assertion $W$ (\emph{world satisfaction}) which ensures th
W \eqdef{}& \Exists I : \mathcal I \fpfn \Prop.
\begin{array}[t]{@{} l}
\ownGhost{\gname_{\textmon{Inv}}}{\authfull
- \mapsingletonComp {\iname}
+ \mapComp {\iname}
{\aginj(\latertinj(\wIso(I(\iname))))}
{\iname \in \dom(I)}} * \\
\Sep_{\iname \in \dom(I)} \left( \later I(\iname) * \ownGhost{\gname_{\textmon{Dis}}}{\set{\iname}} \lor \ownGhost{\gname_{\textmon{En}}}{\set{\iname}} \right)
--
GitLab