From b1465125b491e5f1912e26090af240135bcf1ad8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Sat, 22 Oct 2016 13:54:11 +0200
Subject: [PATCH] docs: make the borders slightly larger, so that lines of text
dont become so ridicolously long and are easier to read
---
docs/iris.tex | 2 +-
docs/model.tex | 5 +++--
2 files changed, 4 insertions(+), 3 deletions(-)
diff --git a/docs/iris.tex b/docs/iris.tex
index 4813b2701..0840b2ae9 100644
--- a/docs/iris.tex
+++ b/docs/iris.tex
@@ -8,7 +8,7 @@
\usepackage[english]{babel}
\usepackage[babel=true]{microtype}
\fi
-\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}
+\usepackage{geometry}
\usepackage[backend=biber]{biblatex}
\bibliography{bib}
diff --git a/docs/model.tex b/docs/model.tex
index 8c085f770..fcb9d7272 100644
--- a/docs/model.tex
+++ b/docs/model.tex
@@ -45,8 +45,9 @@ We are thus going to define the assertions as mapping CMRA elements to sets of s
\Sem{\vctx \proves \All \var : \type. \prop : \Prop}_\gamma &\eqdef
\Lam \melt. \setComp{n}{ \All v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
\Sem{\vctx \proves \Exists \var : \type. \prop : \Prop}_\gamma &\eqdef
- \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) } \\
- ~\\
+ \Lam \melt. \setComp{n}{ \Exists v \in \Sem{\type}. n \in \Sem{\vctx, \var : \type \proves \prop : \Prop}_{\mapinsert \var v \gamma}(\melt) }
+\end{align*}
+\begin{align*}
\Sem{\vctx \proves \prop * \propB : \Prop}_\gamma &\eqdef \Lam\melt. \setComp{n}{\begin{aligned}\Exists \meltB_1, \meltB_2. &\melt \nequiv{n} \meltB_1 \mtimes \meltB_2 \land {}\\& n \in \Sem{\vctx \proves \prop : \Prop}_\gamma(\meltB_1) \land n \in \Sem{\vctx \proves \propB : \Prop}_\gamma(\meltB_2)\end{aligned}}
\\
\Sem{\vctx \proves \prop \wand \propB : \Prop}_\gamma &\eqdef
--
GitLab