% generated by Ott 0.20.3 from: ottalt.ott
\newcommand{\ottdrule}[4][]{{\displaystyle\frac{\begin{array}{l}#2\end{array}}{#3}\quad\ottdrulename{#4}}}
\newcommand{\ottusedrule}[1]{\[#1\]}
\newcommand{\ottpremise}[1]{ #1 \\}
\newenvironment{ottdefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]}{}
\newenvironment{ottfundefnblock}[3][]{ \framebox{\mbox{#2}} \quad #3 \\[0pt]\begin{displaymath}\begin{array}{l}}{\end{array}\end{displaymath}}
\newcommand{\ottfunclause}[2]{ #1 \equiv #2 \\}
\newcommand{\ottnt}[1]{\mathit{#1}}
\newcommand{\ottmv}[1]{\mathit{#1}}
\newcommand{\ottkw}[1]{\mathbf{#1}}
\newcommand{\ottsym}[1]{#1}
\newcommand{\ottcom}[1]{\text{#1}}
\newcommand{\ottdrulename}[1]{\textsc{#1}}
\newcommand{\ottcomplu}[5]{\overline{#1}^{\,#2\in #3 #4 #5}}
\newcommand{\ottcompu}[3]{\overline{#1}^{\,#2<#3}}
\newcommand{\ottcomp}[2]{\overline{#1}^{\,#2}}
\newcommand{\ottgrammartabular}[1]{\begin{supertabular}{llcllllll}#1\end{supertabular}}
\newcommand{\ottmetavartabular}[1]{\begin{supertabular}{ll}#1\end{supertabular}}
\newcommand{\ottrulehead}[3]{$#1$ & & $#2$ & & & \multicolumn{2}{l}{#3}}
\newcommand{\ottprodline}[6]{& & $#1$ & $#2$ & $#3 #4$ & $#5$ & $#6$}
\newcommand{\ottfirstprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
\newcommand{\ottbindspecprodline}[6]{\ottprodline{#1}{#2}{#3}{#4}{#5}{#6}}
\newcommand{\ottprodnewline}{\\}
\newcommand{\ottinterrule}{\\[5.0mm]}
\newcommand{\ottafterlastrule}{\\}
\newcommand{\ottmetavars}{
\ottmetavartabular{
 $ \nonterm x $ & \multicolumn{1}{l}{\ottcom{variables}} \\
 $ \nonterm a $ & \multicolumn{1}{l}{\ottcom{type variables}} \\
}}

\newcommand{\ottt}{
\ottrulehead{\nonterm t}{::=}{\ottcom{types}}\ottprodnewline
\ottfirstprodline{|}{\nonterm a}{}{}{}{\ottcom{type variable}}\ottprodnewline
\ottprodline{|}{\nonterm t_{{\mathrm{1}}}  \to  \nonterm t_{{\mathrm{2}}}}{}{}{}{\ottcom{function}}\ottprodnewline
\ottprodline{|}{\forall \, \nonterm a  \ottsym{.}  \nonterm t}{}{}{}{\ottcom{univeral}}\ottprodnewline
\ottprodline{|}{\ottsym{(}  \nonterm t  \ottsym{)}} {\textsf{S}}{}{}{}}

\newcommand{\otte}{
\ottrulehead{\nonterm e}{::=}{\ottcom{terms}}\ottprodnewline
\ottfirstprodline{|}{\nonterm x}{}{}{}{\ottcom{variable}}\ottprodnewline
\ottprodline{|}{\lambda  \nonterm x  \ottsym{:}  \nonterm t  \ottsym{.}  \nonterm e}{}{}{}{\ottcom{abstraction}}\ottprodnewline
\ottprodline{|}{\nonterm e_{{\mathrm{1}}} \, \nonterm e_{{\mathrm{2}}}}{}{}{}{\ottcom{application}}\ottprodnewline
\ottprodline{|}{\Lambda  \nonterm a  \ottsym{.}  \nonterm e}{}{}{}{\ottcom{type abstraction}}\ottprodnewline
\ottprodline{|}{\nonterm e  \ottsym{[}  \nonterm t  \ottsym{]}}{}{}{}{\ottcom{type application}}\ottprodnewline
\ottprodline{|}{\ottsym{(}  \nonterm e  \ottsym{)}} {\textsf{S}}{}{}{}}

\newcommand{\ottG}{
\ottrulehead{\nonterm G}{::=}{\ottcom{typing contexts}}\ottprodnewline
\ottfirstprodline{|}{\bullet}{}{}{}{\ottcom{empty}}\ottprodnewline
\ottprodline{|}{\nonterm G  \ottsym{,}  \nonterm x  \ottsym{:}  \nonterm t}{}{}{}{\ottcom{variable assumption}}\ottprodnewline
\ottprodline{|}{\ottsym{G,}  \nonterm a}{}{}{}{\ottcom{type variable assumption}}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\ottt\ottinterrule
\otte\ottinterrule
\ottG\ottafterlastrule
}}

% defnss
% defns Jtype
% defn typing
\newcommand{\ottdruleTXXVar}[1]{\ottdrule[#1]{%
\ottpremise{\nonterm x  \ottsym{:}  \nonterm t \, \in \, \nonterm G}%
}{
\nonterm G  \vdash  \nonterm x  \ottsym{:}  \nonterm t}{%
{\ottdrulename{T\_Var}}{}%
}}


\newcommand{\ottdruleTXXAbs}[1]{\ottdrule[#1]{%
\ottpremise{\nonterm G  \ottsym{,}  \nonterm x  \ottsym{:}  \nonterm t_{{\mathrm{1}}}  \vdash  \nonterm e  \ottsym{:}  \nonterm t_{{\mathrm{2}}}}%
}{
\nonterm G  \vdash  \lambda  \nonterm x  \ottsym{:}  \nonterm t_{{\mathrm{1}}}  \ottsym{.}  \nonterm e  \ottsym{:}  \nonterm t_{{\mathrm{1}}}  \to  \nonterm t_{{\mathrm{2}}}}{%
{\ottdrulename{T\_Abs}}{}%
}}


\newcommand{\ottdruleTXXApp}[1]{\ottdrule[#1]{%
\ottpremise{\nonterm G  \vdash  \nonterm e_{{\mathrm{1}}}  \ottsym{:}  \nonterm t'  \to  \nonterm t}%
\ottpremise{\nonterm G  \vdash  \nonterm e_{{\mathrm{2}}}  \ottsym{:}  \nonterm t'}%
}{
\nonterm G  \vdash  \nonterm e_{{\mathrm{1}}} \, \nonterm e_{{\mathrm{2}}}  \ottsym{:}  \nonterm t}{%
{\ottdrulename{T\_App}}{}%
}}


\newcommand{\ottdruleTXXTAbs}[1]{\ottdrule[#1]{%
\ottpremise{\ottsym{G,}  \nonterm a  \vdash  \nonterm e  \ottsym{:}  \nonterm t}%
}{
\nonterm G  \vdash  \Lambda  \nonterm a  \ottsym{.}  \nonterm e  \ottsym{:}  \forall \, \nonterm a  \ottsym{.}  \nonterm t}{%
{\ottdrulename{T\_TAbs}}{}%
}}


\newcommand{\ottdruleTXXTApp}[1]{\ottdrule[#1]{%
\ottpremise{\nonterm G  \vdash  \nonterm e  \ottsym{:}  \forall \, \nonterm a  \ottsym{.}  \nonterm t'}%
\ottpremise{\nonterm G  \vdash  \nonterm t \, \ottkw{ok}}%
}{
\nonterm G  \vdash  \nonterm e  \ottsym{[}  \nonterm t  \ottsym{]}  \ottsym{:}  \ottsym{\{}  \nonterm t  \ottsym{/}  \nonterm a  \ottsym{\}}  \nonterm t'}{%
{\ottdrulename{T\_TApp}}{}%
}}

\newcommand{\ottdefntyping}[1]{\begin{ottdefnblock}[#1]{$\nonterm G  \vdash  \nonterm e  \ottsym{:}  \nonterm t$}{\ottcom{term typing}}
\ottusedrule{\ottdruleTXXVar{}}
\ottusedrule{\ottdruleTXXAbs{}}
\ottusedrule{\ottdruleTXXApp{}}
\ottusedrule{\ottdruleTXXTAbs{}}
\ottusedrule{\ottdruleTXXTApp{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJtype}{
\ottdefntyping{}}

\newcommand{\ottdefnss}{
\ottdefnsJtype}

\newcommand{\ottall}{\ottmetavars\\[0pt]
\ottgrammar\\[5.0mm]
\ottdefnss
}