From 2f8adc23a90f4e22caa5c3bcf18801611a171e3c Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Wed, 6 Sep 2017 12:06:34 -0400 Subject: [PATCH] 11.1: s/smallstep/smallstepo/ to match Coq source https://github.com/achlipala/frap/blob/master/TypesAndMutation.v#L117 allows new/read/overwrite inside contexts --- frap_book.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/frap_book.tex b/frap_book.tex index addbee4..c765b42 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -2954,13 +2954,13 @@ $$\begin{array}{rrcl} \newcommand{\dom}[1]{\mathsf{dom}(#1)} Now we can write the rules for the three reference primitives. -$$\infer{\smallstep{(h, \newref{v})}{(\mupd{h}{\ell}{v}, \ell)}}{ +$$\infer{\smallstepo{(h, \newref{v})}{(\mupd{h}{\ell}{v}, \ell)}}{ \ell \notin \dom{h} } -\quad \infer{\smallstep{(h, \readref{\ell})}{(h, v)}}{ +\quad \infer{\smallstepo{(h, \readref{\ell})}{(h, v)}}{ \msel{h}{\ell} = v } -\quad \infer{\smallstep{(h, \writeref{\ell}{v'})}{(\mupd{h}{\ell}{v'}, v')}}{ +\quad \infer{\smallstepo{(h, \writeref{\ell}{v'})}{(\mupd{h}{\ell}{v'}, v')}}{ \msel{h}{\ell} = v }$$