pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

11.1: s/smallstep/smallstepo/ to match Coq source

Browse source 
https://github.com/achlipala/frap/blob/master/TypesAndMutation.v#L117 allows new/read/overwrite inside contexts
This commit is contained in:
Andres Erbsen 2017-09-06 12:06:34 -04:00 committed by GitHub
parent 103c8ad557
commit 2f8adc23a9
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
frap_book.tex
View file

@ -2954,13 +2954,13 @@ $$\begin{array}{rrcl}
\newcommand{\dom}[1]{\mathsf{dom}(#1)} \newcommand{\dom}[1]{\mathsf{dom}(#1)}
Now we can write the rules for the three reference primitives. 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} \ell \notin \dom{h}
} }
\quad \infer{\smallstep{(h, \readref{\ell})}{(h, v)}}{ \quad \infer{\smallstepo{(h, \readref{\ell})}{(h, v)}}{
\msel{h}{\ell} = 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 \msel{h}{\ell} = v
}$$ }$$