|
|
@ -6547,9 +6547,9 @@ Computations |
|
|
% Let |
|
|
% Let |
|
|
\inferrule*[Lab=\tylab{Let}] |
|
|
\inferrule*[Lab=\tylab{Let}] |
|
|
{\typc{\Delta;\Gamma}{M : A}{E} \\ |
|
|
{\typc{\Delta;\Gamma}{M : A}{E} \\ |
|
|
\typ{\Delta;\Gamma, x : A}{N : C} |
|
|
|
|
|
|
|
|
\typc{\Delta;\Gamma, x : A}{N : B}{E} |
|
|
} |
|
|
} |
|
|
{\typ{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : C}} |
|
|
|
|
|
|
|
|
{\typc{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : B}{E}} |
|
|
\end{mathpar} |
|
|
\end{mathpar} |
|
|
\caption{Typing rules} |
|
|
\caption{Typing rules} |
|
|
\label{fig:base-language-type-rules} |
|
|
\label{fig:base-language-type-rules} |
|
|
|
