Skip to content
Snippets Groups Projects
Commit b0840d3e authored by Max New's avatar Max New
Browse files

include defs!

parent e77e255a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 172 additions and 0 deletions
jfp-paper/defs.tex 0 → 100644
+ 172
− 0
View file @ b0840d3e
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% WARNING: I changed these commands
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\renewcommand{\u}{\underline}
\renewcommand{\sup}[2]{\srho{\upcast{#1}{#2}}}
%% This is a proof that only appears in the long version, and is
%% otherwise completely omitted
\NewEnviron{longproof}{%
\iflong\begin{proof}\BODY \end{proof}\fi%
}
\NewEnviron{longfigure}{%
\iflong\begin{figure}\BODY \end{figure}\fi%
}
\NewEnviron{longonly}{%
\iflong\BODY \fi%
}
\NewEnviron{shortonly}{%
\ifshort\BODY \fi%
}
%% \newtheorem*{nonnum-theorem}{Theorem}
\newcommand{\cbpv}{CBPV}
\newcommand{\cbpvstar}{CBPV*}
\newcommand{\cbpvtxt}{\cbpv}
\newcommand{\sem}[1]{\llbracket#1\rrbracket}
\newcommand{\sdncast}[2]{\sem{\dncast{#1}{#2}}}
\newcommand{\supcast}[2]{\sem{\upcast{#1}{#2}}}
\newcommand{\srho}[1]{\sem{#1}_\rho}
\newcommand{\sdn}[2]{\srho{\dncast{#1}{#2}}}
\newcommand{\hetplug}[1]{\langle#1\rangle}
\newcommand{\nats}{\mathbb{N}}
\newtheorem{principle}{Principle}
\newcommand{\vtype}{\,\,\text{val type}}
\newcommand{\ctype}{\,\,\text{comp type}}
\newcommand{\ctx}{\,\,\text{ctx}}
\newcommand{\stoup}{\,\,\text{stoup}}
\newcommand{\pipe}{\,\,|\,\,}
\newcommand{\hole}{\bullet}
\newcommand{\floor}[1]{\lfloor#1\rfloor}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\precltdyn}{\mathrel{\preceq\ltdyn}}
\newcommand{\precgtdyn}{\mathrel{\preceq\gtdyn}}
\newcommand{\ltdynsucc}{\mathrel{\ltdyn\succeq}}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
\newcommand{\ltlogty}[2]{\mathrel{\ltdyn^{#1}_{#2}}}
\newcommand{\logpole}{\mathrel{\lesssim^{log}_{\pole}}}
\newcommand{\pole}{\Bot}
\newcommand{\ipole}[1]{\mathrel{\pole^{#1}}}
\newcommand{\logc}[1]{\mathrel{\pole}^{#1}}
\newcommand{\logty}[2]{\mathrel{\lesssim^{#1}_{#2,\pole}}}
\newcommand{\ltlogc}[1]{\mathrel{\ltdyn^{#1}_{\vdash}}}
\newcommand{\ltctx}{\mathrel{\ltdyn^{ctx}}}
\newcommand{\ltciu}{\mathrel{\ltdyn^{ciu}}}
\newcommand{\ltlog}{\mathrel{\ltdyn^{log}}}
\newcommand{\apreorder}{\trianglelefteq}
\newcommand{\ctxpreorder}{\mathrel{\apreorder^{\text{ctx}}}}
\newcommand{\ctxize}[1]{\mathrel{{#1}^{\text{ctx}}}}
\newcommand{\ix}[2]{\mathrel{#1^{#2}}}
\newcommand{\simsub}[1]{\mathrel{\sim_{#1}}}
\newcommand{\itylrof}[3]{\ilrof{#1}{#3,#2}}
\newcommand{\ilrof}[2]{\mathrel{{#1}^{\text{log}}_{#2}}}
\newcommand{\itylr}[2]{\itylrof{\apreorder}{#1}{#2}}
\newcommand{\ilr}[1]{\ilrof{\apreorder}{#1}}
\newcommand{\simp}[1]{{#1}^{\dag}}
\newcommand{\simpp}[1]{\simp{({#1})}}
%% Operational steps
\newcommand{\step}{\mapsto}
\newcommand{\stepsin}[1]{\mathrel{\mapsto^{#1}}}
\newcommand{\stepzero}{\stepsin 0}
\newcommand{\stepone}{\stepsin 1}
\newcommand{\stepstar}{\stepsin{*}}
\newcommand{\bigstepsin}[1]{\mathrel{\Mapsto^{#1}}}
\newcommand{\bigstepzero}{\bigstepsin{0}}
\newcommand{\bigstepany}{\bigstepsin{}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\pairone}[1]{\{ \pi \mapsto {#1}}
\newcommand{\pairtwo}[1]{\pipe \pi' \mapsto {#1}\}}
\newcommand{\emptypair}[0]{\{\}}
\newcommand{\pairWtoXYtoZ}[4]{\{ #1 \mapsto {#2} \pipe #3 \mapsto {#4}\}}
\newcommand{\tru}{\texttt{true}}
\newcommand{\fls}{\texttt{false}}
\newcommand{\ifXthenYelseZ}[3]{\kw{if}#1\,\kw{then}#2\,\kw{else}#3}
\newcommand{\bool}{\mathbb{B}}
\newcommand{\inl}{\kw{inl}}
\newcommand{\inr}{\kw{inr}}
\newcommand{\intag}[1]{\texttt{in}_{#1}}
\newcommand{\els}{\kw {else}}
\newcommand{\seq}{\texttt{seq}}
\newcommand{\dyn}{{?}}
\newcommand{\dynv}{{?}}
\newcommand{\dync}{\u {\text{?`}}}
\newcommand{\uarrow}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\darrow}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
\newcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
\newcommand{\obcast}[2]{\langle{#1}\Leftarrow{#2}\rangle}
\newcommand{\err}{\mho}
\newcommand{\diverge}{\Omega}
\newcommand{\print}{\kw{print}}
\newcommand{\roll}{\kw{roll}}
\newcommand{\rollty}[1]{\texttt{roll}_{#1}\,\,}
\newcommand{\unroll}{\kw{unroll}}
\newcommand{\unrollty}[1]{\texttt{unroll}_{#1}\,\,}
\newcommand{\defupcast}[2]{\langle\kern-1ex~\langle{#2}\uarrow{#1}\rangle\kern-1ex~\rangle}
\newcommand{\defdncast}[2]{\langle\kern-1ex~\langle{#1}\darrow{#2}\rangle\kern-1ex~\rangle}
\newcommand{\result}{\text{result}}
\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\kw{let}}
\newcommand{\letXbeYinZ}[2]{\lett#2 = #1;}
\newcommand{\bindXtoYinZ}[2]{\kw{bind}#2 \leftarrow #1;}
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\caseofX}[1]{\case #1}
\newcommand{\thenY}{\{}
\newcommand{\elseZ}[1]{\pipe #1 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
\newcommand{\ret}{\kw{ret}}
\newcommand{\thunk}{\kw{thunk}}
\newcommand{\force}{\kw{force}}
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathbin{\&}}
\newcommand{\dyncaseofXthenOnePairSumU}[5]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \pipe #5 \}}
\newcommand{\dyncaseofXthenYelseZ}[3]{\kw{tycase} #1\,\{ #2 \pipe #3 \}}
\newcommand{\dyncocaseWithFunF}[3]{\{\with \mapsto #1 \pipe (\to) \mapsto #2 \pipe \u F \mapsto #3 \}}
\newcommand{\dyncaseofXthenBoolUPair}[4]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \}}
\newcommand{\dyncocaseFunF}[2]{\{(\to) \mapsto #1 \pipe \u F \mapsto #2 \}}
\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
\newcommand{\alt}{\bnfalt}
\newcommand{\bnfdef}{\mathrel{\bf ::=}}
\newcommand{\bnfadd}{\mathrel{\bf +::=}}
\newcommand{\bnfsub}{\mathrel{\bf -::=}}
\newcommand\dynvctx[0]{\mathsf{dyn\mathord{-}vctx}}
\newcommand\dyncctx[0]{\mathsf{dyn\mathord{-}cctx}}
\newcommand\leastdynv[0]{\bot_{\mathsf{v}}}
\newcommand\leastdync[0]{\bot_{\mathsf{c}}}
\newcommand\errordivergeleft[0]{\preceq\ltdyn}
\newcommand\errordivergeright[0]{\ltdyn\succeq}
\newcommand\errordivergerightop[0]{\preceq\gtdyn}
\newcommand\bvtopv[1]{#1^{c}}
\newcommand\bvtopvpure[1]{#1^{v}}
\newcommand\purely{\downarrow}
%% Local Variables:
%% compile-command: "./latexrun jfp-gtt.tex"
%% End:
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