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

Fixes

Browse Source
This commit is contained in:
Andreas Stadelmeier 2024-02-02 13:22:55 +01:00
parent edc7f87108
commit 67ce9e42a2
2 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
tRules.tex
View File

@ -302,7 +302,7 @@ $\begin{array}{l}
\Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad \Delta = \overline{\type{X} : \bot .. \type{U}} \quad \quad
\Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad \Delta \vdash \ol{U}, \ol{T} \ \ok \quad \quad
\Delta \vdash \type{N} \ \ok \quad \quad \Delta \vdash \type{N} \ \ok \quad \quad
\Delta \vdash \ol{M} \ \ok \texttt{in C} \Delta \vdash \ol{M} \ \ok \texttt{ in C}
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\

10
unify.tex
View File

@ -1003,13 +1003,13 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
\rulename{GenDelta} \rulename{GenDelta}
& $ & $
\deduction{ \deduction{
\wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{N} } \implies \Delta, \sigma \wildcardEnv \vdash C \cup \set{\tv{b} \lessdot \type{T} } \implies \Delta, \sigma
}{ }{
\wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{N}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}} \wildcardEnv \vdash [\type{B}/\tv{b}]C \implies \Delta \cup \set{\wildcard{B}{\type{T}}{\bot}}, \sigma \cup \set{\tv{b} \to \type{B}}
} \quad } \quad
\begin{array}{l} \begin{array}{l}
\tph(\type{N}) = \emptyset, \text{fv}(\type{N}) \subseteq \Delta \cup \Delta_in \\ \tph(\type{T}) = \emptyset, \text{fv}(\type{T}) \subseteq \Delta \cup \Delta_{in} \\
\rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta \vdash \type{N} \ \ok \rwildcard{B} \ \text{fresh}, \tv{b} \notin \text{dom}(\sigma), \Delta, \Delta_{in} \vdash \type{T} \ \ok
\end{array} \end{array}
$ $
\\\\ \\\\
@ -1041,7 +1041,7 @@ Otherwise the generation rules \rulename{GenSigma} and \rulename{GenDelta} will
} \quad } \quad
\begin{array}{l} \begin{array}{l}
\tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that \tph(\type{T}) = \emptyset \\ %,\, \text{fv}(\type{T}) \subseteq \Delta \\ % T ok implies that
\tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_in \vdash \type{T} \ \ok \tv{a} \notin \text{dom}(\sigma),\, \Delta, \Delta_{in} \vdash \type{T} \ \ok
\end{array} \end{array}
$ $
\\\\ \\\\