Skip to content
GitLab
Menu
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
23c54a27
Commit
23c54a27
authored
Feb 09, 2016
by
Ralf Jung
Browse files
heap_lang: get rid of some unnecessary parenthesis
parent
ee1c154a
Changes
1
Hide whitespace changes
Inline
Side-by-side
heap_lang/tests.v
View file @
23c54a27
...
...
@@ -53,9 +53,9 @@ Module LiftingTests.
Qed
.
Definition
FindPred
(
n2
:
expr
)
:
expr
:=
rec
::
(
let
:
#
1
+
Lit
1
in
if
#
0
<
n2
.[
ren
(
+
3
)]
then
#
1
#
0
else
#
2
)
.
rec
::
let
:
#
1
+
Lit
1
in
if
#
0
<
n2
.[
ren
(
+
3
)]
then
#
1
#
0
else
#
2.
Definition
Pred
:
expr
:=
λ
:
(
if
#
0
≤
Lit
0
then
Lit
0
else
FindPred
#
0
(
Lit
0
)
)
%
L
.
λ
:
if
#
0
≤
Lit
0
then
Lit
0
else
FindPred
#
0
(
Lit
0
).
Lemma
FindPred_spec
n1
n2
E
Q
:
(
■
(
n1
<
n2
)
∧
Q
(
LitV
$
pred
n2
))
⊑
wp
E
(
FindPred
(
Lit
n2
)
(
Lit
n1
))
Q
.
...
...
Write
Preview
Supports
Markdown
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