stan/Ecoop2024_TIforWildFJ
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Change prepare rule to require same type on both sides

Browse Source
This commit is contained in:
JanUlrich 2024-01-17 05:52:01 +01:00
parent bc4fcaf43c
commit 56f9d35615
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
unify.tex
View File

@ -380,15 +380,15 @@ Their upper and lower bounds are fresh type variables.
\begin{array}[c]{@{}ll}
\begin{array}[c]{l}
\wildcardEnv \vdash
C \cup \, \set{ \wcNtype{\Delta}{S} \lessdot \wcNtype{\Delta'}{N} } \\
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdot \wctype{\Delta'}{C}{\ol{T}} } \\
\hline
\vspace*{-0.4cm}\\
\wildcardEnv \vdash
C \cup \, \set{ \wcNtype{\Delta}{S} \lessdotCC \wcNtype{\Delta'}{N} } \\
C \cup \, \set{ \wctype{\Delta}{C}{\ol{S}} \lessdotCC \wctype{\Delta'}{C}{\ol{T}} } \\
\end{array}
%\quad \ol{Y} = \textit{fresh}(\ol{X})
\quad \begin{array}[c]{l}
\text{fv}(\wcNtype{\Delta}{S}, \wcNtype{\Delta'}{N}) = \emptyset
\text{fv}(\wctype{\Delta}{C}{\ol{S}}, \wctype{\Delta'}{C}{\ol{T}}) = \emptyset
\end{array}
\end{array}
$