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

Change rules so Completeness proof is possible

Browse Source
This commit is contained in:
JanUlrich 2024-04-02 00:09:52 +02:00
parent 87f413241a
commit 3620f0c781
1 changed files with 7 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
tRules.tex
View File

@ -460,15 +460,18 @@ $\begin{array}{l}
\end{array}$ \end{array}$
\\[1em] \\[1em]
$\begin{array}{l} $\begin{array}{l}
%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair<X,Y>?
%TODO: we do not allow X.Pair<X,X> in the t-let (could we allow it? what about L and U being WTVs?)
\typerule{T-Let}\\ \typerule{T-Let}\\
\begin{array}{@{}c} \begin{array}{@{}c}
\Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad \Delta | \Gamma \vdash \expr{t}_1 : \type{T}_1 \quad \quad
\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N} %\Delta \vdash \type{T}_1 <: \wcNtype{\Delta'}{N}
\Delta \vdash \type{T}_1 <: \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}}
\\ \\
\Delta, \Delta' | \Gamma, \expr{x} : \wcNtype{}{N} \vdash \expr{t}_2 : \type{T}_2 \quad \quad \Delta, \Delta' | \Gamma, \expr{x} : \wctype{}{C}{\ol{X}} \vdash \expr{t}_2 : \type{T}_2 \quad \quad
\Delta, \Delta' \vdash \type{T}_2 <: \type{T} \quad \quad \Delta, \Delta' \vdash \type{T}_2 <: \type{T} \quad \quad
\text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad % \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad
\Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok
\\ \\
\hline \hline
\vspace*{-0.3cm}\\ \vspace*{-0.3cm}\\