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
Joshua Yanovski
iris-coq
Commits
595b0419
Commit
595b0419
authored
Feb 15, 2016
by
Robbert Krebbers
Browse files
Most language notation keywords include a colon: now if does too.
parent
858a5949
Changes
2
Hide whitespace changes
Inline
Side-by-side
heap_lang/notation.v
View file @
595b0419
...
...
@@ -39,7 +39,7 @@ Notation "'rec:' f x := e" := (Rec f x e%L)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
lang_scope
.
Notation
"'rec:' f x := e"
:=
(
RecV
f
x
e
%
L
)
(
at
level
102
,
f
at
level
1
,
x
at
level
1
,
e
at
level
200
)
:
lang_scope
.
Notation
"'if' e1 'then' e2 'else' e3"
:=
(
If
e1
%
L
e2
%
L
e3
%
L
)
Notation
"'if
:
' e1 'then' e2 'else' e3"
:=
(
If
e1
%
L
e2
%
L
e3
%
L
)
(
at
level
200
,
e1
,
e2
,
e3
at
level
200
)
:
lang_scope
.
(
**
Derived
notions
,
in
order
of
declaration
.
The
notations
for
let
and
seq
...
...
heap_lang/tests.v
View file @
595b0419
...
...
@@ -51,10 +51,10 @@ Section LiftingTests.
Definition
FindPred
:
val
:=
rec:
"pred"
"x"
"y"
:=
let:
"yp"
:=
"y"
+
'1
in
if
"yp"
<
"x"
then
"pred"
"x"
"yp"
else
"y"
.
if
:
"yp"
<
"x"
then
"pred"
"x"
"yp"
else
"y"
.
Definition
Pred
:
val
:=
λ
:
"x"
,
if
"x"
≤
'0
then
-
FindPred
(
-
"x"
+
'
2
)
'0
else
FindPred
"x"
'0
.
if
:
"x"
≤
'0
then
-
FindPred
(
-
"x"
+
'
2
)
'0
else
FindPred
"x"
'0
.
Lemma
FindPred_spec
n1
n2
E
Q
:
(
■
(
n1
<
n2
)
∧
Q
'
(
n2
-
1
))
⊑
wp
E
(
FindPred
'
n2
'
n1
)
Q
.
...
...
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