Commit a5200723 authored by Edward Z. Yang's avatar Edward Z. Yang

OK, I think we've finally solved granularity.

Signed-off-by: default avatarEdward Z. Yang <ezyang@cs.stanford.edu>
parent 612d948b
This diff is collapsed.
This diff is collapsed.
%% hide the full syntax of shapes/types for the paper
\newcommand{\fullmsh}[3]{\aoxb{#1 ~\mtypsep~ #2 ~\mtypsep~ #3}}
\newcommand{\fullmtyp}[3]{
\aoxb{\mtypsepsp #1 \mtypsepsp\mtypsep\mtypsepsp
#2 \mtypsepsp\mtypsep\mtypsepsp
#3 \mtypsepsp}}
\newcommand{\fullbigmtyp}[3]{\ensuremath{
\left\langle\!\vrule \begin{array}{l}
#1 ~\mtypsep \\[0pt]
#2 ~\mtypsep \\
#3
\end{array} \vrule\!\right\rangle
}}
\renewcommand{\msh}[2]{\aoxb{#1 \mtypsepsp\mtypsep\mtypsepsp #2}}
\renewcommand{\mtyp}[2]{
\aoxb{#1 ~\mtypsep~ #2}}
\newcommand{\mtypstretch}[2]{
\left\langle\!\vrule
\mtypsepsp #1 \mtypsepsp\mtypsep\mtypsepsp #2 \mtypsepsp
\vrule\!\right\rangle
}
\renewcommand{\bigmtyp}[2]{\ensuremath{
\left\langle\!\vrule \begin{array}{l}
#1 ~\mtypsep \\[0pt] #2
\end{array} \vrule\!\right\rangle
}}
%% change syntax of signatures
\renewcommand{\Esig}[1]{\ensuremath{\,[#1]}}
\renewcommandx*{\JBVSh}[3][1=\Delta, usedefault=@]%
{#1 \vdashsh #2 \Rightarrow #3}
% JUDGMENTS
\renewcommandx*{\JBTypElab}[6][1=\Delta, 2=\Gamma, 3=\shctx, usedefault=@]%
% {\JBTyp[#1][#2][#3]{#4}{#5} \elabto #6}
{\JBTyp[#1][#2][#3]{#4}{#5} \;\shade{\elabto #6}}
\renewcommandx*{\JBVTypElab}[5][1=\Delta, 2=\shctx, usedefault=@]%
% {\JBVTyp[#1][#2]{#3}{#4} \elabto #5}
{\JBVTyp[#1][#2]{#3}{#4} \;\shade{\elabto #5}}
\renewcommandx*{\JDTypElab}[4][1=\Delta, usedefault=@]%
% {#1 \vdash #2 : #3 \elabto #4}
{#1 \vdash #2 : #3 \;\shade{\elabto #4}}
\renewcommandx*{\JCModElab}[5][1=\Gamma, 2=\nu_0, usedefault=@]%
% {#1; #2 \vdashghc #3 : #4 \elabto #5}
{#1; #2 \vdashghc #3 : #4 \;\shade{\elabto #5}}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "paper"
%%% End:
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