Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
Actris
Commits
1b3eb3df
Commit
1b3eb3df
authored
Apr 25, 2019
by
Jonas Kastberg Hinrichsen
Browse files
Bumped Examples
parent
796090cc
Changes
1
Hide whitespace changes
Inline
Side-by-side
theories/examples.v
View file @
1b3eb3df
...
...
@@ -7,7 +7,7 @@ From iris.base_logic Require Import invariants.
Section
Examples
.
Context
`
{!
heapG
Σ
}
(
N
:
namespace
).
Context
`
{!
logrelG
Σ
}.
Context
`
{!
logrelG
val
Σ
}.
Notation
"⟦ c @ s : sτ ⟧{ γ }"
:
=
(
interp_st
N
γ
s
τ
c
s
)
(
at
level
10
,
s
at
next
level
,
s
τ
at
next
level
,
γ
at
next
level
,
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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