From d7cae999437be665757ee3a26f0084347b09d704 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 Mar 2016 18:28:22 +0100
Subject: [PATCH] docs: update iris.sty
---
docs/constructions.tex | 2 +-
docs/iris.sty | 2 ++
2 files changed, 3 insertions(+), 1 deletion(-)
diff --git a/docs/constructions.tex b/docs/constructions.tex
index 939281c8b..0afec08f2 100644
--- a/docs/constructions.tex
+++ b/docs/constructions.tex
@@ -6,7 +6,7 @@
Given some COFE $\cofe$, we define $\agm(\cofe)$ as follows:
\begin{align*}
- \monoid \eqdef{}& \setComp{(c, V) \subseteq (\mathbb{N} \to T) \times \mathbb{N}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V } \\
+ \monoid \eqdef{}& \setComp{(c, V) \in (\mathbb{N} \to T) \times \pset{\mathbb{N}}}{ \All n, m. n \geq m \Ra n \in V \Ra m \in V } \\
& \text{quotiented by} \\
(c_1, V_1) \equiv (c_1, V_2) \eqdef{}& V_1 = V_2 \land \All n. n \in V_1 \Ra c_1(n) \nequiv{n} c_2(n) \\
(c_1, V_1) \nequiv{n} (c_1, V_2) \eqdef{}& (\All m \leq n. m \in V_1 \Lra m \in V_2) \land (\All m \leq n. m \in V_1 \Ra c_1(m) \nequiv{m} c_2(m)) \\
diff --git a/docs/iris.sty b/docs/iris.sty
index b5e3df222..5b3721f46 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -106,10 +106,12 @@
%% Some commonly used identifiers
+\newcommand{\SProp}{\textdom{SProp}}
\newcommand{\UPred}{\textdom{UPred}}
\newcommand{\mProp}{\textdom{Prop}} % meta-level prop
\newcommand{\iProp}{\textdom{iProp}}
\newcommand{\Wld}{\textdom{Wld}}
+\newcommand{\Res}{\textdom{Res}}
\newcommand{\cofe}{T}
\newcommand{\cofeB}{U}
--
GitLab