From 3620f0c7818d4a2d7536e3fe272ac27b0e8170d1 Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Tue, 2 Apr 2024 00:09:52 +0200 Subject: [PATCH] Change rules so Completeness proof is possible --- tRules.tex | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/tRules.tex b/tRules.tex index ff727c8..6cc565f 100644 --- a/tRules.tex +++ b/tRules.tex @@ -460,15 +460,18 @@ $\begin{array}{l} \end{array}$ \\[1em] $\begin{array}{l} +%TODO: why is dom(\Delta) subset of fv(N) a restriction. This excludes X,Y^X.Pair? +%TODO: we do not allow X.Pair in the t-let (could we allow it? what about L and U being WTVs?) \typerule{T-Let}\\ \begin{array}{@{}c} \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 - \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad - \Delta \vdash \type{T}, \wcNtype{\Delta'}{N} \ \ok + % \text{dom}(\Delta') \subseteq \text{fv}(\type{N}) \quad \quad + \Delta \vdash \type{T}, \wctype{\overline{\wildcard{X}{\type{U}}{\type{L}}}}{C}{\ol{X}} \ \ok \\ \hline \vspace*{-0.3cm}\\