From 3e0feccae8f773872ff851182ca3b4841805d639 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 May 2022 12:48:40 +0200
Subject: [PATCH] add a test document for our macros
---
tex/test.tex | 32 ++++++++++++++++++++++++++++++++
1 file changed, 32 insertions(+)
create mode 100644 tex/test.tex
diff --git a/tex/test.tex b/tex/test.tex
new file mode 100644
index 000000000..256e13e20
--- /dev/null
+++ b/tex/test.tex
@@ -0,0 +1,32 @@
+\documentclass[10pt]{article}
+\usepackage{lmodern}
+\usepackage[T1]{fontenc}
+\usepackage[utf8]{inputenc}
+
+\input{setup}
+
+
+\title{The Iris TeX Test Document}
+\begin{document}
+\maketitle
+
+Here we put a bunch of uses of the macros in \texttt{iris.sty} that we can visually test to ensure they still work when those macros are changed.
+
+{
+\newcommand{\mapstoDisk}{\mapsto_d}
+\newcommand{\mapstoOp}{\mapsto_{\mathit{op}}}
+\newcommand{\mapstoLftd}{\mapsto_d^{\mathrm{lftd}}}
+
+\begin{align*}
+ \hoareV{ \begin{aligned}
+ &\dom(m) = \dom(m') * {} \\
+ &\left( \Sep_{(a,o) \in m} a \mapstoLftd o \right) * %
+ \left( \Sep_{(a,o') \in m'} a \mapstoOp o' \right)
+ \end{aligned}} %
+ {\mathit{op}.\texttt{Commit}()}%
+ {\left( \Sep_{(a,o) \in m} a \mapstoDisk o \right) \lor
+ \left( \Sep_{(a,o') \in m'} a \mapstoDisk o' \right) }
+\end{align*}
+}
+
+\end{document}
--
GitLab