pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Merge pull request #20 from andres-erbsen/patch-1

Browse source 
11.1: s/smallstep/smallstepo/ to match Coq source
This commit is contained in:
Adam Chlipala 2017-09-10 14:05:46 -04:00 committed by GitHub
commit 19e9e84953
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
}$$ }$$