Commit 072803bc authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'docs-geometry' into 'master'

docs: make the borders slightly larger

This makes it so that lines of text don't become so ridiculously long and are easier to read.

What do you think @robbertkrebbers @jjourdan ?

See merge request !17
parents 17d6e030 b1465125
......@@ -8,7 +8,7 @@
\usepackage[top=1in, bottom=1in, left=1.25in, right=1.25in]{geometry}
......@@ -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) }
\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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment