From a44568f789a9aeeca8c70e4a17d8929dda2656ff Mon Sep 17 00:00:00 2001 From: JanUlrich Date: Wed, 24 Jul 2024 10:16:30 +0200 Subject: [PATCH] Combine let and field access in soundness proof --- soundness.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/soundness.tex b/soundness.tex index 7859104..9f4b849 100644 --- a/soundness.tex +++ b/soundness.tex @@ -134,12 +134,13 @@ By structural induction over the expression $\texttt{e}$. Therefore we can say $\Delta,\Delta' | \Gamma, \expr{x}:\type{N} \vdash \expr{t}_2 : \sigma(\tv{e}_2)$ by assumption and $\Delta, \Delta' \vdash \sigma(\tv{e}_2) <: \sigma(\tv{a})$ by lemma \ref{lemma:unifySoundness} given the constraint $\tv{e}_2 \lessdot \tv{a}$. - \item[$\expr{v}.\texttt{f}$] + \item[$\texttt{let}\ \texttt{x} = \texttt{t}_1 \ \texttt{in}\ \expr{x}.\texttt{f}$] %TODO: use a lemma that says if Unify succeeds, then it also succeeds if the capture converted types are used. % but it also works with a subset of the initial constraints. % the generated constraints do not share wildcard placehodlers with other constraints. % can they contain free variables from other places? They could, but isolation prevents that. % TODO: but how to proof? +%generated constraints: t1 <. x, x <. N, T <. t2 We are allowed to use capture conversion for $\expr{v}$ here. $\Delta \vdash \expr{v} : \sigma(\tv{a})$ by assumption. $\Delta \vdash \sigma(\tv{a}) <: \sigma(\exptype{C}{\ol{\wtv{a}}})$ and