% generated by Ott 0.10.14 from: ../tests/test8.ott
\documentclass[11pt]{article}
\usepackage{amsmath,amssymb}
\usepackage{supertabular}
\usepackage{geometry}
\usepackage{ifthen}
\geometry{%
a4paper,
% letterpaper,
dvips,
twoside,
left=22.5mm, right=22.5mm,
top=20mm,  bottom=30mm,
}
\usepackage{color}
\begin{document}
\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{\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{\ottinterrule}{\\[5.0mm]}
\newcommand{\ottafterlastrule}{\\}
\newcommand{\ottmetavars}{
\ottmetavartabular{
 $ \ottmv{value\_name} ,\, \ottmv{x} $ &  \\
 $ \ottmv{ident} $ &  \\
 $ \ottmv{integer\_literal} $ &  \\
 $ \ottmv{index} ,\, \ottmv{i} ,\, \ottmv{j} ,\, \ottmv{n} ,\, \ottmv{m} $ &  \\
}}

\newcommand{\otttypeconstr}{
\ottrulehead{\ottnt{typeconstr}}{::=}{}\\ 
\ottprodline{|}{\ottkw{unit}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{bool}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{int}}{}{}{}{}}

\newcommand{\otttypvar}{
\ottrulehead{\ottnt{typvar}  ,\ \ottnt{tv}}{::=}{}\\ 
\ottprodline{|}{' \, \ottmv{ident}}{}{}{}{}}

\newcommand{\otttypexpr}{
\ottrulehead{\ottnt{typexpr}  ,\ \ottnt{t}}{::=}{}\\ 
\ottprodline{|}{\ottnt{typvar}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typexpr} \, \rightarrow \, \ottnt{typexpr'}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typeconstr}}{}{}{}{}\\ 
\ottprodline{|}{( \, \ottnt{typexpr} \, )} {\textsf{S}}{}{}{}}

\newcommand{\otttypscheme}{
\ottrulehead{\ottnt{typscheme}  ,\ \ottnt{ts}}{::=}{}\\ 
\ottprodline{|}{( \, \ottnt{typvar_{{\mathrm{1}}}} \, , \, .. \, , \, \ottnt{typvar_{\ottmv{n}}} \, ) \, \ottnt{typexpr}}{}{\textsf{bind}\; \ottnt{typvar_{{\mathrm{1}}}}..\ottnt{typvar_{\ottmv{n}}}\; \textsf{in}\; \ottnt{typexpr}}{}{}\\ 
\ottprodline{|}{\ottkw{generalise} \, ( \, \Gamma \, , \, \ottnt{t} \, )} {\textsf{M}}{}{}{}}

\newcommand{\ottconstant}{
\ottrulehead{\ottnt{constant}  ,\ \ottnt{c}}{::=}{}\\ 
\ottprodline{|}{\ottmv{integer\_literal}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{false}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{true}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{()}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{(\&\&)}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{not}}{}{}{}{}}

\newcommand{\ottexpr}{
\ottrulehead{\ottnt{expr}  ,\ \ottnt{e}}{::=}{}\\ 
\ottprodline{|}{\ottmv{value\_name}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{constant}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{expr} \, \ottnt{expr'}}{}{}{}{}\\ 
\ottprodline{|}{\textbf{function} \, \ottmv{value\_name} \, \rightarrow \, \ottnt{expr}}{}{\textsf{bind}\; \ottmv{value\_name}\; \textsf{in}\; \ottnt{expr}}{}{}\\ 
\ottprodline{|}{\ottkw{let} \, \ottmv{value\_name} \, = \, \ottnt{expr} \, \ottkw{in} \, \ottnt{expr'}}{}{\textsf{bind}\; \ottmv{value\_name}\; \textsf{in}\; \ottnt{expr'}}{}{}\\ 
\ottprodline{|}{( \, \ottnt{expr} \, )} {\textsf{S}}{}{}{}\\ 
\ottprodline{|}{\{ \, \ottnt{v} \, / \, \ottmv{x} \, \} \, \ottnt{e}} {\textsf{M}}{}{}{}}

\newcommand{\ottvalue}{
\ottrulehead{\ottnt{value}  ,\ \ottnt{v}}{::=}{}\\ 
\ottprodline{|}{\ottnt{constant}}{}{}{}{}\\ 
\ottprodline{|}{\textbf{function} \, \ottmv{value\_name} \, \rightarrow \, \ottnt{expr}}{}{}{}{}}

\newcommand{\ottG}{
\ottrulehead{\Gamma}{::=}{}\\ 
\ottprodline{|}{\ottkw{empty}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, , \, \ottmv{value\_name} \, : \, \ottnt{typscheme}}{}{}{}{}}

\newcommand{\ottformula}{
\ottrulehead{\ottnt{formula}}{::=}{}\\ 
\ottprodline{|}{\ottnt{judgement}}{}{}{}{}\\ 
\ottprodline{|}{\ottkw{not} \, ( \, \ottnt{formula} \, )}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typscheme} \, > \, \ottnt{t}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typscheme} \, = \, \ottnt{typscheme'}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{value\_name} \, = \, \ottmv{value\_name'}}{}{}{}{}}

\newcommand{\ottterminals}{
\ottrulehead{\ottnt{terminals}}{::=}{}\\ 
\ottprodline{|}{ \rightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \textbf{function} }{}{}{}{}\\ 
\ottprodline{|}{ \vdash }{}{}{}{}\\ 
\ottprodline{|}{ \longrightarrow }{}{}{}{}\\ 
\ottprodline{|}{ \{ }{}{}{}{}\\ 
\ottprodline{|}{ \} }{}{}{}{}}

\newcommand{\ottJtype}{
\ottrulehead{\ottnt{Jtype}}{::=}{}\\ 
\ottprodline{|}{\ottmv{value\_name} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{constant} \, : \, \ottnt{t}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma \, \vdash \, \ottnt{e} \, : \, \ottnt{t}}{}{}{}{}}

\newcommand{\ottJop}{
\ottrulehead{\ottnt{Jop}}{::=}{}\\ 
\ottprodline{|}{\ottnt{e} \, \longrightarrow \, \ottnt{e'}}{}{}{}{}}

\newcommand{\ottjudgement}{
\ottrulehead{\ottnt{judgement}}{::=}{}\\ 
\ottprodline{|}{\ottnt{Jtype}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{Jop}}{}{}{}{}}

\newcommand{\ottuserXXsyntax}{
\ottrulehead{\ottnt{user\_syntax}}{::=}{}\\ 
\ottprodline{|}{\ottmv{value\_name}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{ident}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{integer\_literal}}{}{}{}{}\\ 
\ottprodline{|}{\ottmv{index}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typeconstr}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typvar}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typexpr}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{typscheme}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{constant}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{expr}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{value}}{}{}{}{}\\ 
\ottprodline{|}{\Gamma}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{formula}}{}{}{}{}\\ 
\ottprodline{|}{\ottnt{terminals}}{}{}{}{}}

\newcommand{\ottgrammar}{\ottgrammartabular{
\otttypeconstr\ottinterrule
\otttypvar\ottinterrule
\otttypexpr\ottinterrule
\otttypscheme\ottinterrule
\ottconstant\ottinterrule
\ottexpr\ottinterrule
\ottvalue\ottinterrule
\ottG\ottinterrule
\ottformula\ottinterrule
\ottterminals\ottinterrule
\ottJtype\ottinterrule
\ottJop\ottinterrule
\ottjudgement\ottinterrule
\ottuserXXsyntax\ottafterlastrule
}}

% defnss
% defns Jtype
% defn VTSin
\newcommand{\ottdruleVTSinXXvnOne}[1]{\ottdrule[#1]{%
}{
\ottmv{value\_name} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma \, , \, \ottmv{value\_name} \, : \, \ottnt{typscheme}}{
{\ottdrulename{VTSin\_vn1}}{}
}}


\newcommand{\ottdruleVTSinXXvnTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottmv{value\_name} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma}%
\ottpremise{\ottkw{not} \, ( \, \ottmv{value\_name} \, = \, \ottmv{value\_name'} \, )}%
}{
\ottmv{value\_name} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma \, , \, \ottmv{value\_name'} \, : \, \ottnt{typscheme'}}{
{\ottdrulename{VTSin\_vn2}}{}
}}

\newcommand{\ottdefnVTSin}[1]{\begin{ottdefnblock}[#1]{$\ottmv{value\_name} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma$}{}
\ottusedrule{\ottdruleVTSinXXvnOne{}}
\ottusedrule{\ottdruleVTSinXXvnTwo{}}
\end{ottdefnblock}}


% defn G_constant
\newcommand{\ottdruleconstantXXint}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottmv{integer\_literal} \, : \, \ottkw{int}}{
{\ottdrulename{constant\_int}}{}
}}


\newcommand{\ottdruleconstantXXfalse}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottkw{false} \, : \, \ottkw{bool}}{
{\ottdrulename{constant\_false}}{}
}}


\newcommand{\ottdruleconstantXXtrue}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottkw{true} \, : \, \ottkw{bool}}{
{\ottdrulename{constant\_true}}{}
}}


\newcommand{\ottdruleconstantXXunit}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottkw{()} \, : \, \ottkw{unit}}{
{\ottdrulename{constant\_unit}}{}
}}


\newcommand{\ottdruleconstantXXand}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottkw{(\&\&)} \, : \, \ottkw{bool} \, \rightarrow \, ( \, \ottkw{bool} \, \rightarrow \, \ottkw{bool} \, )}{
{\ottdrulename{constant\_and}}{}
}}


\newcommand{\ottdruleconstantXXnot}[1]{\ottdrule[#1]{%
}{
\Gamma \, \vdash \, \ottkw{not} \, : \, \ottkw{bool} \, \rightarrow \, \ottkw{bool}}{
{\ottdrulename{constant\_not}}{}
}}

\newcommand{\ottdefnGXXconstant}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{constant} \, : \, \ottnt{t}$}{}
\ottusedrule{\ottdruleconstantXXint{}}
\ottusedrule{\ottdruleconstantXXfalse{}}
\ottusedrule{\ottdruleconstantXXtrue{}}
\ottusedrule{\ottdruleconstantXXunit{}}
\ottusedrule{\ottdruleconstantXXand{}}
\ottusedrule{\ottdruleconstantXXnot{}}
\end{ottdefnblock}}


% defn Get
\newcommand{\ottdruleGetXXvalueXXname}[1]{\ottdrule[#1]{%
\ottpremise{\ottmv{x} \, : \, \ottnt{typscheme} \, \ottkw{in} \, \Gamma}%
\ottpremise{\ottnt{typscheme} \, > \, \ottnt{t}}%
}{
\Gamma \, \vdash \, \ottmv{x} \, : \, \ottnt{t}}{
{\ottdrulename{Get\_value\_name}}{}
}}


\newcommand{\ottdruleGetXXconstant}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{constant} \, : \, \ottnt{t}}%
}{
\Gamma \, \vdash \, \ottnt{constant} \, : \, \ottnt{t}}{
{\ottdrulename{Get\_constant}}{}
}}


\newcommand{\ottdruleGetXXapply}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{e} \, : \, \ottnt{t_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{t_{{\mathrm{2}}}}}%
\ottpremise{\Gamma \, \vdash \, \ottnt{e'} \, : \, \ottnt{t_{{\mathrm{1}}}}}%
}{
\Gamma \, \vdash \, \ottnt{e} \, \ottnt{e'} \, : \, \ottnt{t_{{\mathrm{2}}}}}{
{\ottdrulename{Get\_apply}}{}
}}


\newcommand{\ottdruleGetXXlambda}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, , \, \ottmv{x_{{\mathrm{1}}}} \, : \, ( \, \, \, ) \, \ottnt{t_{{\mathrm{1}}}} \, \vdash \, \ottnt{e} \, : \, \ottnt{t}}%
}{
\Gamma \, \vdash \, \textbf{function} \, \ottmv{x_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{e} \, : \, \ottnt{t_{{\mathrm{1}}}} \, \rightarrow \, \ottnt{t}}{
{\ottdrulename{Get\_lambda}}{}
}}


\newcommand{\ottdruleGetXXlet}[1]{\ottdrule[#1]{%
\ottpremise{\Gamma \, \vdash \, \ottnt{e} \, : \, \ottnt{t}}%
\ottpremise{\Gamma \, , \, \ottmv{x} \, : \, \ottnt{typscheme} \, \vdash \, \ottnt{e'} \, : \, \ottnt{t'}}%
\ottpremise{\ottnt{typscheme} \, = \, \ottkw{generalise} \, ( \, \Gamma \, , \, \ottnt{t} \, )}%
}{
\Gamma \, \vdash \, \ottkw{let} \, \ottmv{x} \, = \, \ottnt{e} \, \ottkw{in} \, \ottnt{e'} \, : \, \ottnt{t'}}{
{\ottdrulename{Get\_let}}{}
}}

\newcommand{\ottdefnGet}[1]{\begin{ottdefnblock}[#1]{$\Gamma \, \vdash \, \ottnt{e} \, : \, \ottnt{t}$}{}
\ottusedrule{\ottdruleGetXXvalueXXname{}}
\ottusedrule{\ottdruleGetXXconstant{}}
\ottusedrule{\ottdruleGetXXapply{}}
\ottusedrule{\ottdruleGetXXlambda{}}
\ottusedrule{\ottdruleGetXXlet{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJtype}{
\ottdefnVTSin{}
\ottdefnGXXconstant{}
\ottdefnGet{}}


% defns Jop
% defn red
\newcommand{\ottdruleJOXXredXXapp}[1]{\ottdrule[#1]{%
}{
( \, \textbf{function} \, \ottmv{x} \, \rightarrow \, \ottnt{e} \, ) \, \ottnt{v} \, \longrightarrow \, \{ \, \ottnt{v} \, / \, \ottmv{x} \, \} \, \ottnt{e}}{
{\ottdrulename{JO\_red\_app}}{}
}}


\newcommand{\ottdruleJOXXredXXlet}[1]{\ottdrule[#1]{%
}{
\ottkw{let} \, \ottmv{x} \, = \, \ottnt{v} \, \ottkw{in} \, \ottnt{e} \, \longrightarrow \, \{ \, \ottnt{v} \, / \, \ottmv{x} \, \} \, \ottnt{e}}{
{\ottdrulename{JO\_red\_let}}{}
}}


\newcommand{\ottdruleJOXXredXXcontextXXappOne}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{e} \, \longrightarrow \, \ottnt{e'}}%
}{
\ottnt{e} \, \ottnt{e_{{\mathrm{1}}}} \, \longrightarrow \, \ottnt{e'} \, \ottnt{e_{{\mathrm{1}}}}}{
{\ottdrulename{JO\_red\_context\_app1}}{}
}}


\newcommand{\ottdruleJOXXredXXcontextXXappTwo}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{e} \, \longrightarrow \, \ottnt{e'}}%
}{
\ottnt{v} \, \ottnt{e} \, \longrightarrow \, \ottnt{v} \, \ottnt{e'}}{
{\ottdrulename{JO\_red\_context\_app2}}{}
}}


\newcommand{\ottdruleJOXXredXXcontextXXlet}[1]{\ottdrule[#1]{%
\ottpremise{\ottnt{e} \, \longrightarrow \, \ottnt{e'}}%
}{
\ottkw{let} \, \ottmv{x} \, = \, \ottnt{e} \, \ottkw{in} \, \ottnt{e_{{\mathrm{1}}}} \, \longrightarrow \, \ottkw{let} \, \ottmv{x} \, = \, \ottnt{e'} \, \ottkw{in} \, \ottnt{e_{{\mathrm{1}}}}}{
{\ottdrulename{JO\_red\_context\_let}}{}
}}


\newcommand{\ottdruleJOXXredXXnotXXOne}[1]{\ottdrule[#1]{%
}{
\ottkw{not} \, \ottkw{true} \, \longrightarrow \, \ottkw{false}}{
{\ottdrulename{JO\_red\_not\_1}}{}
}}


\newcommand{\ottdruleJOXXredXXnotXXTwo}[1]{\ottdrule[#1]{%
}{
\ottkw{not} \, \ottkw{false} \, \longrightarrow \, \ottkw{true}}{
{\ottdrulename{JO\_red\_not\_2}}{}
}}


\newcommand{\ottdruleJOXXredXXandXXOne}[1]{\ottdrule[#1]{%
}{
( \, \ottkw{(\&\&)} \, \ottkw{true} \, ) \, \ottnt{e} \, \longrightarrow \, \ottnt{e}}{
{\ottdrulename{JO\_red\_and\_1}}{}
}}


\newcommand{\ottdruleJOXXredXXandXXTwo}[1]{\ottdrule[#1]{%
}{
( \, \ottkw{(\&\&)} \, \ottkw{false} \, ) \, \ottnt{e} \, \longrightarrow \, \ottkw{false}}{
{\ottdrulename{JO\_red\_and\_2}}{}
}}

\newcommand{\ottdefnJOXXred}[1]{\begin{ottdefnblock}[#1]{$\ottnt{e} \, \longrightarrow \, \ottnt{e'}$}{}
\ottusedrule{\ottdruleJOXXredXXapp{}}
\ottusedrule{\ottdruleJOXXredXXlet{}}
\ottusedrule{\ottdruleJOXXredXXcontextXXappOne{}}
\ottusedrule{\ottdruleJOXXredXXcontextXXappTwo{}}
\ottusedrule{\ottdruleJOXXredXXcontextXXlet{}}
\ottusedrule{\ottdruleJOXXredXXnotXXOne{}}
\ottusedrule{\ottdruleJOXXredXXnotXXTwo{}}
\ottusedrule{\ottdruleJOXXredXXandXXOne{}}
\ottusedrule{\ottdruleJOXXredXXandXXTwo{}}
\end{ottdefnblock}}


\newcommand{\ottdefnsJop}{
\ottdefnJOXXred{}}

\newcommand{\ottdefnss}{
\ottdefnsJtype
\ottdefnsJop}

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

\ottall
\begin{verbatim}
Definition rules:        22 good    0 bad
Definition rule clauses: 36 good    0 bad
\end{verbatim}
\end{document}