Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Iris
Iris
Commits
467c44e4
Commit
467c44e4
authored
Oct 14, 2016
by
Jacques-Henri Jourdan
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq
parents
2a4baa1d
5a5c2e9e
Pipeline
#2833
passed with stage
in 9 minutes and 22 seconds
Changes
1
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
4 additions
and
4 deletions
+4
-4
docs/base-logic.tex
docs/base-logic.tex
+4
-4
No files found.
docs/base-logic.tex
View file @
467c44e4
...
...
@@ -376,18 +376,18 @@ Furthermore, we have the usual $\eta$ and $\beta$ laws for projections, $\lambda
\paragraph
{
Laws for the resource update modality.
}
\begin{mathpar}
\infer
[
upd-mono
]
\infer
H
{
upd-mono
}
{
\prop
\proves
\propB
}
{
\upd\prop
\proves
\upd\propB
}
\infer
[
upd-intro
]
\infer
H
{
upd-intro
}
{}{
\prop
\proves
\upd
\prop
}
\infer
[
upd-trans
]
\infer
H
{
upd-trans
}
{}
{
\upd
\upd
\prop
\proves
\upd
\prop
}
\infer
[
upd-frame
]
\infer
H
{
upd-frame
}
{}{
\propB
*
\upd\prop
\proves
\upd
(
\propB
*
\prop
)
}
\inferH
{
upd-update
}
...
...
Write
Preview
Markdown
is supported
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