Skip to content

Commit

Permalink
Fix orphan on page 20
Browse files Browse the repository at this point in the history
  • Loading branch information
jeremie-koenig committed Dec 9, 2024
1 parent f308acc commit 50f1e43
Showing 1 changed file with 6 additions and 9 deletions.
15 changes: 6 additions & 9 deletions compcertoe/compcertoe.tex
Original file line number Diff line number Diff line change
Expand Up @@ -4349,16 +4349,13 @@ \subsection{State Encapsulation}
Hidden state allows us to define an \emph{encapsulation} primitive
$[ u \rangle : U \lensarrow \mathbbm{1}$,
which can be composed in front of a strategy
which can be used
to turn an explicit state component into a private one.
The component $[u\rangle$ uses $P := U$ for its persistent state.
When it is first activated
by an incoming question $* \in \mathbbm{1}$,
the initial state $u \in U$ is used on the outgoing side.
Whenever an updated $u' \in U$ is received,
the component stores $u'$ as its next persistent state.
This primitive uses $P := U$ for its persistent state.
When it is activated by $* \in \mathbbm{1}$,
the current state (initially $u \in U$) is used as an outgoing question;
the answer $u' \in U$
is then used as an updated state for the next activation.
%}}}
Expand Down

0 comments on commit 50f1e43

Please sign in to comment.