Changeset 2424
 Timestamp:
 Oct 31, 2012, 12:59:12 PM (7 years ago)
 Location:
 Papers/polymorphicvariants2012
 Files:

 1 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

Papers/polymorphicvariants2012/polymorphicvariants.tex
r2416 r2424 3 3 \smartqed 4 4 5 \usepackage{amsmath} 5 6 \usepackage[english]{babel} 6 7 \usepackage[colorlinks]{hyperref} 7 8 \usepackage{listings} 8 9 \usepackage{microtype} 10 \usepackage{prooftree} 11 12 \newcommand{\ent}{\vdash} 13 \newcommand{\funarr}{\rightarrow} 14 \newcommand{\lam}[2]{\lambda{#1}.{#2}} 15 \newcommand{\letin}[3]{\mathbf{let}\ {#1}\ {:=}\ {#2}\ \mathbf{in}\ {#3}} 16 \newcommand{\pair}[2]{\langle #1, #2 \rangle} 17 \newcommand{\rulefont}[1]{\ensuremath{(\mathbf{#1})}} 9 18 10 19 \lstset{basicstyle=\footnotesize\tt,columns=flexible,breaklines=false, … … 118 127 \item Bounded vs notbounded. 119 128 \end{itemize} 129 130 \begin{figure} 131 \begin{gather*} 132 \begin{prooftree} 133 (\Gamma(x) = \phi) 134 \justifies 135 K; \Gamma \ent x : \phi 136 \using\rulefont{{\Gamma}x} 137 \end{prooftree} 138 \qquad 139 \begin{prooftree} 140 K; \Gamma, x : \phi \ent r : \psi 141 \justifies 142 K; \Gamma \ent \lam{x}r : \phi \funarr \psi 143 \using\rulefont{{\Gamma}\lambda} 144 \end{prooftree} 145 \qquad 146 \begin{prooftree} 147 K;\Gamma \ent r : \phi \funarr \psi \quad K;\Gamma \ent s : \phi 148 \justifies 149 K;\Gamma \ent rs : \psi 150 \using\rulefont{{\Gamma}rs} 151 \end{prooftree} 152 \\[1.5ex] 153 \begin{prooftree} 154 K; \Gamma \ent r : \phi \quad K; \Gamma, x:\phi \ent s : \psi 155 \justifies 156 K; \Gamma \ent \letin{x}{r}{s} : \psi 157 \using\rulefont{{\Gamma}{:=}} 158 \end{prooftree} 159 \qquad 160 \begin{prooftree} 161 (L \subseteq L' \quad H \subseteq H') 162 \justifies 163 K \oplus i_{{\geq \pair{L}{U}}} \ent i \geq \pair{L'}{H'} 164 \using\rulefont{{K}i} 165 \end{prooftree} 166 \end{gather*} 167 \caption{Garrigue's typing relation for polymorphic variants} 168 \label{fig.garrigue.typing.relation} 169 \end{figure} 120 170 121 171 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
Note: See TracChangeset
for help on using the changeset viewer.