blob: 96ad2bb2cc30b237922dcb6ffc10c421bd894b17 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
%% 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:
|
