Commit bb499fdd authored by Ralf Jung's avatar Ralf Jung

make sure macros do not leak across files

parent 5c232f1e
-Q . ""
s-Q . ""
prelude/option.v
prelude/fin_map_dom.v
prelude/bsets.v
......
......@@ -38,17 +38,17 @@
%\clearpage
\tableofcontents
\clearpage
\clearpage\begingroup
\input{algebra}
\clearpage
\endgroup\clearpage\begingroup
\input{constructions}
\clearpage
\endgroup\clearpage\begingroup
\input{logic}
\clearpage
\endgroup\clearpage\begingroup
\input{model}
\clearpage
\endgroup\clearpage\begingroup
\input{derived}
\clearpage\printbibliography % If we want biblatex
\endgroup\clearpage\begingroup
\printbibliography
\end{document}
......@@ -106,13 +106,12 @@ to express that $\sigfn$ is a function symbol with the indicated arity.
\paragraph{Syntax.}
Iris syntax is built up from a signature $\Sig$ and a countably infinite set $\textdom{Var}$ of variables (ranged over by metavariables $x$, $y$, $z$):
\newcommand{\unitterm}{()}%
\newcommand{\unitsort}{1}% \unit is bold.
\begin{align*}
\term, \prop, \pred ::={}&
x \mid
\sigfn(\term_1, \dots, \term_n) \mid
\unitterm \mid
\unitval \mid
(\term, \term) \mid
\pi_i\; \term \mid
\Lam x.\term \mid
......@@ -174,7 +173,7 @@ We introduce additional metavariables ranging over terms and generally let the c
\]
\paragraph{Variable conventions.}
We often abuse notation, using the preceding \emph{term} metavariables to range over (bound) \emph{variables}.
We often abuse notation, using the preceding \emph{term} meta-variables to range over (bound) \emph{variables}.
We omit type annotations in binders, when the type is clear from context.
......@@ -211,7 +210,7 @@ In writing $\vctx, x:\sort$, we presuppose that $x$ is not already declared in $
}
%%% products
\and
\axiom{\vctx \proves \wtt{\unitterm}{\unitsort}}
\axiom{\vctx \proves \wtt{\unitval}{\unitsort}}
\and
\infer{\vctx \proves \wtt{\term}{\sort_1} \and \vctx \proves \wtt{\termB}{\sort_2}}
{\vctx \proves \wtt{(\term,\termB)}{\sort_1 \times \sort_2}}
......
......@@ -11,7 +11,7 @@ an equivalence relation over $X$ satisfying
\item $\All x,x',n. x \nequiv{n+1} x' \implies x \nequiv{n} x',$
\item $\All x,x'. (\All n. x\nequiv{n} x') \implies x = x'.$
\end{itemize}
\a
Let $(X,(\nequivset{n}{X})_{n\in\mathbb{N}})$ and
$(Y,(\nequivset{n}{Y})_{n\in\mathbb{N}})$ be o.f.e.'s. A function $f:
X\to Y$ is \emph{non-expansive} if, for all $x$, $x'$ and $n$,
......@@ -431,7 +431,7 @@ $\rho\nequiv{n} \rho' \iff n=0 \lor \bigl(\dom(\rho)=\dom(\rho') \land
\Lam v : \Sem{\sort}. \Sem{\vctx, x : \sort \proves \term : \sort'}_{\gamma[x \mapsto v]} \\
\Sem{\vctx \proves \term~\termB : \sort'}_\gamma &=
\Sem{\vctx \proves \term : \sort \to \sort'}_\gamma(\Sem{\vctx \proves \termB : \sort}_\gamma) \\
\Sem{\vctx \proves \unitterm : \unitsort}_\gamma &= \star \\
\Sem{\vctx \proves \unitval : \unitsort}_\gamma &= \star \\
\Sem{\vctx \proves (\term_1, \term_2) : \sort_1 \times \sort_2}_\gamma &= (\Sem{\vctx \proves \term_1 : \sort_1}_\gamma, \Sem{\vctx \proves \term_2 : \sort_2}_\gamma) \\
\Sem{\vctx \proves \pi_i~\term : \sort_1}_\gamma &= \pi_i(\Sem{\vctx \proves \term : \sort_1 \times \sort_2}_\gamma)
\end{align*}
......
......@@ -307,6 +307,8 @@
\newcommand{\mask}{\mathcal{E}}
%% various pieces of Syntax
\newcommand{\unitsort}{1}% \unit is bold.
\def\MU #1.{\mu #1.\;}%
\def\Lam #1.{\lambda #1.\;}%
......
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