From 3438581826f61e9ac004ea386a008a6ee2fab916 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Tue, 25 May 2021 13:03:22 +0100 Subject: [PATCH] Reword --- thesis.tex | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/thesis.tex b/thesis.tex index 14dc684..c93df25 100644 --- a/thesis.tex +++ b/thesis.tex @@ -6749,7 +6749,7 @@ elaboration for top-level function types. \begin{equations} \trval{-} &:& \ValTypeCat \to \ValTypeCat\\ \trval{A \to B \eff E} &\defas& \pval{A}_{E'} \to \pval{B}_{E'} \eff E'\\ - \multicolumn{3}{l}{\quad\where~E' = (\xval{A} \blacktriangleright E) \blacktriangleright (\xval{B} \blacktriangleright E)} + \multicolumn{3}{l}{\quad\where~E' = (\xval{A} \blacktriangleright E) \vartriangleright (\xval{B} \blacktriangleright E)} \end{equations} % The function $\trval{-}$ traverses the abstract syntax of its argument @@ -6757,6 +6757,9 @@ twice. The first traversal propagates effect information outwards to the ambient effect row $E$. The second traversal pushes the full ambient information $E'$ inwards. % +The construction of $E'$ makes use of the fact that +$E \vartriangleright E = E$. +% As a remark, note that the function $\trval{-}$ do not have to consider handler types, because they cannot appear at the top-level in $\HCalc$. With this syntactic sugar in place we can program with