Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Joseph Tassarotti
iris-coq-public
Commits
2c6e9fa6
Commit
2c6e9fa6
authored
Nov 14, 2017
by
Joseph Tassarotti
Browse files
Fix typo in value case of weakest pre documentation.
parent
2f0164f4
Changes
1
Hide whitespace changes
Inline
Side-by-side
docs/program-logic.tex
View file @
2c6e9fa6
...
@@ -257,7 +257,7 @@ This can be instantiated, for example, with ownership of an authoritative RA to
...
@@ -257,7 +257,7 @@ This can be instantiated, for example, with ownership of an authoritative RA to
\begin{align*}
\begin{align*}
\textdom
{
wp
}
\eqdef
{}&
\MU
\textdom
{
wp
}
.
\Lam
\mask
,
\expr
,
\pred
.
\\
\textdom
{
wp
}
\eqdef
{}&
\MU
\textdom
{
wp
}
.
\Lam
\mask
,
\expr
,
\pred
.
\\
&
(
\Exists\val
.
\toval
(
\expr
) =
\val
\land
\pvs
[\mask]
\pr
op
)
\lor
{}
\\
&
(
\Exists\val
.
\toval
(
\expr
) =
\val
\land
\pvs
[\mask]
\pr
ed
(
\val
)
)
\lor
{}
\\
&
\Bigl
(
\toval
(
\expr
) =
\bot
\land
\All
\state
. I(
\state
)
\vsW
[\mask][\emptyset]
{}
\\
&
\Bigl
(
\toval
(
\expr
) =
\bot
\land
\All
\state
. I(
\state
)
\vsW
[\mask][\emptyset]
{}
\\
&
\qquad
\red
(
\expr
,
\state
) *
\later\All
\expr
',
\state
',
\vec\expr
. (
\expr
,
\state
\step
\expr
',
\state
',
\vec\expr
)
\vsW
[\emptyset][\mask]
{}
\\
&
\qquad
\red
(
\expr
,
\state
) *
\later\All
\expr
',
\state
',
\vec\expr
. (
\expr
,
\state
\step
\expr
',
\state
',
\vec\expr
)
\vsW
[\emptyset][\mask]
{}
\\
&
\qquad\qquad
I(
\state
') *
\textdom
{
wp
}
(
\mask
,
\expr
',
\pred
) *
\Sep
_{
\expr
''
\in
\vec\expr
}
\textdom
{
wp
}
(
\top
,
\expr
'',
\Lam
\any
.
\TRUE
)
\Bigr
)
\\
&
\qquad\qquad
I(
\state
') *
\textdom
{
wp
}
(
\mask
,
\expr
',
\pred
) *
\Sep
_{
\expr
''
\in
\vec\expr
}
\textdom
{
wp
}
(
\top
,
\expr
'',
\Lam
\any
.
\TRUE
)
\Bigr
)
\\
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment