From 357686800a45a8d8a285f1851398c1906173ac26 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 8 Apr 2018 14:15:51 -0400 Subject: [PATCH] Proofreading TypesAndMutation --- frap_book.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/frap_book.tex b/frap_book.tex index 279c6f1..11b4861 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -3154,7 +3154,7 @@ More precisely, the limit on how many times we can run garbage collection in a r The type-safety proof is fairly straightforward to update. We prove progress by \emph{ignoring} the garbage-collection rule, since the existing rules were already enough to find a step for every nonvalue. -A bit more work is needed to update the proof of preservation; its case for the existing rules follows the same way as before, while we must prove a few lemmas on the way to handling the new rule. +A bit more work is needed to update the proof of preservation; its cases for the existing rules follow the same way as before, while we must prove a few lemmas on the way to handling the new rule. \begin{lemma}[Transitivity for reachability] If $\freeloc{e_1} \subseteq \freeloc{e_2}$, then $\reach{h}{e_1} \subseteq \reach{h}{e_2}$.