thufschmitt/tix-papers
1
1
Fork 0
mirror of https://github.com/thufschmitt/tix-papers.git synced 2024-08-16 08:10:41 +03:00
Code Issues Projects Releases Wiki Activity

Remove definiton of the obsolete matchType symbol

Browse Source
This commit is contained in:
regnat 2017-05-11 07:36:31 +02:00
parent 2bd9a4ac58
commit cfa357647c
1 changed files with 0 additions and 57 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

57
typing/type-system.tex
View File

@ -94,63 +94,6 @@ and~\pref{typing::operators}.
\caption{Typing rules for the patterns\label{typing::patterns::typing-rules}}
\end{figure}
\begin{figure}
\begin{center}
\begin{tabular}{rl}
\eqdefa{$\matchType{x}$}{$\any$}{}
\eqdefa{$\matchType{q@x}$}{$\matchType{q}$}{}
\eqdefa{$\matchType{\{ f_1, \cdots, f_n \}}$}%
{$\{ \matchType{f_1}; \cdots \matchType{f_n}; \}$}{}
\eqdefa{$\matchType{l}$}{$l = \any$}{}
\eqdefa{$\matchType{l ? e}$}{$l = \any \vee \undef$}{}
\eqdefa{$\matchType{\text{Cons}(x_1, x_2)}$}{$\text{Cons}(\any, \any)$}{}
\end{tabular}
\end{center}
\caption{Semantics of the $\matchType{\_}$ operator%
\label{typing::pattern-accept}}
\end{figure}
\begin{figure}
\begin{tabular}{rl}
\eqdefa{$\ofTypeP{x}{\τ}$}{$\sfrac{x}{\τ}$}{}
\eqdefa{$\ofTypeP{q@x}{\τ}$}{$\sfrac{x}{\τ}; \ofTypeP{q}{x}$}{}
\eqdefa{$\ofTypeP{\{\}}{\{ x_1 ? c_1, \cdots, x_n ? c_n \}}$}{%
$\sfrac{x_1}{\mathcal{B}(c_1)}; \cdots; \sfrac{x_n}{\mathcal{B}(c_n)}$}{}
\eqdefa{%
$\ofTypeP{%
\{ s_1 = \τ_1; \cdots; s_m = \τ_m; \}%
}{%
\{x_1 ? c_1, \cdots, x_n ? c_n, \textbf{\ldots}\}%
}$%
}{%
$\sfrac{x_1}{\mathcal{B}(c_1)}; \cdots; \sfrac{x_n}{\mathcal{B}(c_n)}$%
}{%
if %
$\forall (i,j) \in \discrete{1}{m} \times \discrete{1}{n}, s_i \neq s_j$%
}
\eqdefa{$\ofTypeP{\{ s = \τ;\}}{\{ x \}}$}{$\sfrac{x}{\τ}$}{if $s = x$}
\eqdefa{$\ofTypeP{\{ s = \τ;\}}{\{ x ? c \}}$}{$\sfrac{x}{\τ}$}{if $s = x$}
\eqdefa{$%
\ofTypeP{\{ s_1 = \τ_1; \cdots; s_n = \τ_n \}}{\{ x, f_1, \cdots, f_m \}}%
$}{$%
\sfrac{x}{\τ};%
\ofTypeP{\{ s_2 = \τ_2; \cdots; s_n = \τ_n \}}{\{ f_1, \cdots, f_m \}}%
$}{if $s_1 = x$}
\eqdefa{
$\ofTypeP{%
\{ s_1 = \τ_1; \cdots; s_n = \τ_n \}}%
{\{ x ? c, f_1 \cdots, f_m \}}$%
}{%
$\sfrac{x}{\τ};%
\ofTypeP{\{ s_2 = \τ_2; \cdots; s_n = \τ_n \}}%
{\{ f_1, \cdots, f_m \}}$%
}{if $s_1 = x$}
\eqdefa{%
$\ofTypeP{\text{Cons}(\τ_1, \τ_2)}{\text{Cons}(x_1, x_2)}$%
}{$\sfrac{x_1}{\τ_1}; \sfrac{x_2}{\τ_2}$}{}
\end{tabular}
\caption{Semantics of $\ofTypeP{p}{\τ}$%
\label{typing::pattern-ty-match}}
\end{figure}
\begin{figure}
\input{typing/lambdaCalculus}
\caption{Typing rules for the $\λ\&-calculus$\label{typing::lambda-calculus}}