mirror of
https://github.com/achlipala/frap.git
synced 2024-11-10 00:07:51 +00:00
Proofreading TypesAndMutation
This commit is contained in:
parent
2cb852b29c
commit
357686800a
1 changed files with 1 additions and 1 deletions
|
@ -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}$.
|
||||
|
|
Loading…
Reference in a new issue