Add Trim method
This commit is contained in:
parent
10fcfcfea0
commit
7bf8a3a2da
19
unify.tex
19
unify.tex
@ -444,6 +444,25 @@ Their upper and lower bounds are fresh type variables.
|
|||||||
\end{array}
|
\end{array}
|
||||||
$
|
$
|
||||||
\\\\
|
\\\\
|
||||||
|
\rulename{Trim}
|
||||||
|
&
|
||||||
|
$
|
||||||
|
\begin{array}[c]{@{}ll}
|
||||||
|
\begin{array}[c]{l}
|
||||||
|
\wildcardEnv \vdash
|
||||||
|
C \cup \, \set{ \wctype{\Delta,\Delta'}{C}{\ol{S}} \lessdot \type{T} } \\
|
||||||
|
\hline
|
||||||
|
\vspace*{-0.4cm}\\
|
||||||
|
\wildcardEnv \vdash
|
||||||
|
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \type{T} } \\
|
||||||
|
\end{array}
|
||||||
|
%\quad \ol{Y} = \textit{fresh}(\ol{X})
|
||||||
|
\quad \begin{array}[c]{l}
|
||||||
|
\text{fv}(\ol{S}) \cap \Delta' = \emptyset
|
||||||
|
\end{array}
|
||||||
|
\end{array}
|
||||||
|
$
|
||||||
|
\\\\
|
||||||
% \rulename{Adopt}
|
% \rulename{Adopt}
|
||||||
% & $
|
% & $
|
||||||
% \begin{array}[c]{@{}ll}
|
% \begin{array}[c]{@{}ll}
|
||||||
|
Loading…
Reference in New Issue
Block a user