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
George Pirlea
Iris
Commits
f96a894b
Commit
f96a894b
authored
Sep 09, 2017
by
Robbert Krebbers
Browse files
Set notation scopes of some language stuff.
parent
bcb1b03d
Changes
2
Hide whitespace changes
Inline
Side-by-side
theories/program_logic/ectx_language.v
View file @
f96a894b
...
...
@@ -36,12 +36,12 @@ Class EctxLanguage (expr val ectx state : Type) := {
exists
K''
,
K'
=
comp_ectx
K
K''
;
}.
Arguments
of_val
{
_
_
_
_
_
}
_
.
Arguments
to_val
{
_
_
_
_
_
}
_
.
Arguments
of_val
{
_
_
_
_
_
}
_
%
V
.
Arguments
to_val
{
_
_
_
_
_
}
_
%
E
.
Arguments
empty_ectx
{
_
_
_
_
_
}.
Arguments
comp_ectx
{
_
_
_
_
_
}
_
_
.
Arguments
fill
{
_
_
_
_
_
}
_
_
.
Arguments
head_step
{
_
_
_
_
_
}
_
_
_
_
_
.
Arguments
fill
{
_
_
_
_
_
}
_
_
%
E
.
Arguments
head_step
{
_
_
_
_
_
}
_
%
E
_
_
%
E
_
_
.
Arguments
to_of_val
{
_
_
_
_
_
}
_
.
Arguments
of_to_val
{
_
_
_
_
_
}
_
_
_
.
...
...
theories/program_logic/ectxi_language.v
View file @
f96a894b
...
...
@@ -26,10 +26,10 @@ Class EctxiLanguage (expr val ectx_item state : Type) := {
head_step
(
fill_item
Ki
e
)
σ
1 e2
σ
2
efs
→
is_Some
(
to_val
e
)
;
}.
Arguments
of_val
{
_
_
_
_
_
}
_
.
Arguments
to_val
{
_
_
_
_
_
}
_
.
Arguments
fill_item
{
_
_
_
_
_
}
_
_
.
Arguments
head_step
{
_
_
_
_
_
}
_
_
_
_
_
.
Arguments
of_val
{
_
_
_
_
_
}
_
%
V
.
Arguments
to_val
{
_
_
_
_
_
}
_
%
E
.
Arguments
fill_item
{
_
_
_
_
_
}
_
_
%
E
.
Arguments
head_step
{
_
_
_
_
_
}
_
%
E
_
_
%
E
_
_
.
Arguments
to_of_val
{
_
_
_
_
_
}
_
.
Arguments
of_to_val
{
_
_
_
_
_
}
_
_
_
.
...
...
@@ -101,3 +101,5 @@ Section ectxi_language.
LanguageCtx
(
ectx_lang
expr
)
(
fill_item
Ki
).
Proof
.
change
(
LanguageCtx
_
(
fill
[
Ki
])).
apply
_
.
Qed
.
End
ectxi_language
.
Arguments
fill
{
_
_
_
_
_
}
_
_
%
E
.
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