diff --git a/docs/iris.tex b/docs/iris.tex index 4813b2701d568ce4d350f269b1f7fe1c796308d5..0840b2ae9bea086882d5d3e62e1a8ceff63fb3a9 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 8c085f770e8b7ed9f8855039e18c790824402555..fcb9d7272614f9f1981ca557a0f20394ca01f16a 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