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
Rice Wine
Iris
Commits
ffd67c09
Commit
ffd67c09
authored
Jun 30, 2018
by
Ralf Jung
Browse files
bind scope before defining notation, to make sure the scope is set for the notation
parent
de86652f
Changes
2
Hide whitespace changes
Inline
Side-by-side
tests/heap_lang.v
View file @
ffd67c09
...
...
@@ -19,6 +19,8 @@ Section tests.
end
.
Qed
.
Definition
val_scope_test_1
:
=
SOMEV
(#(),
#()).
Definition
heap_e
:
expr
:
=
let
:
"x"
:
=
ref
#
1
in
"x"
<-
!
"x"
+
#
1
;;
!
"x"
.
...
...
theories/heap_lang/lang.v
View file @
ffd67c09
...
...
@@ -66,11 +66,11 @@ Inductive expr :=
|
CAS
(
e0
:
expr
)
(
e1
:
expr
)
(
e2
:
expr
)
|
FAA
(
e1
:
expr
)
(
e2
:
expr
).
Bind
Scope
expr_scope
with
expr
.
Notation
NONE
:
=
(
InjL
(
Lit
LitUnit
))
(
only
parsing
).
Notation
SOME
x
:
=
(
InjR
x
)
(
only
parsing
).
Bind
Scope
expr_scope
with
expr
.
Fixpoint
is_closed
(
X
:
list
string
)
(
e
:
expr
)
:
bool
:
=
match
e
with
|
Var
x
=>
bool_decide
(
x
∈
X
)
...
...
@@ -97,11 +97,11 @@ Inductive val :=
|
InjLV
(
v
:
val
)
|
InjRV
(
v
:
val
).
Bind
Scope
val_scope
with
val
.
Notation
NONEV
:
=
(
InjLV
(
LitV
LitUnit
))
(
only
parsing
).
Notation
SOMEV
x
:
=
(
InjRV
x
)
(
only
parsing
).
Bind
Scope
val_scope
with
val
.
Fixpoint
of_val
(
v
:
val
)
:
expr
:
=
match
v
with
|
RecV
f
x
e
=>
Rec
f
x
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