From a1cf5cb9da76a4ae1651a1f51ecffa971b856812 Mon Sep 17 00:00:00 2001
From: Ralf Jung
Date: Mon, 18 Feb 2019 13:51:33 +0100
Subject: [PATCH] we need unlocked value lambdas
---
HeapLang.md | 10 +++++-----
theories/heap_lang/lib/par.v | 2 +-
2 files changed, 6 insertions(+), 6 deletions(-)
diff --git a/HeapLang.md b/HeapLang.md
index 0ac3a23b..b9f2cd11 100644
--- a/HeapLang.md
+++ b/HeapLang.md
@@ -117,11 +117,11 @@ The normal `e1 ||| e2` notation uses expression lambdas, because clearly we want
value lambda). However, the *specification* for parallel composition should use
value lambdas, because prior to applying it the term will be reduced as much as
possible to achieve a normal form. To facilitate this, we define a copy of the
-`e1 ||| e2` notation in the value scope that uses value lambdas. This is not
-actually a value, but we still but it in the value scope to differentiate from
-the other notation that uses expression lambdas. (In the future, we might
-decide to add a separate scope for this.) Then, we write the canonical
-specification using the notation in the value scope.
+`e1 ||| e2` notation in the value scope that uses *unlocked* value lambdas.
+This is not actually a value, but we still but it in the value scope to
+differentiate from the other notation that uses expression lambdas. (In the
+future, we might decide to add a separate scope for this.) Then, we write the
+canonical specification using the notation in the value scope.
This works very well for non-recursive notions. For `while` loops, the
situation is unfortunately more complex and proving the desired specification
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 558853f4..d073142e 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,7 +12,7 @@ Definition par : val :=
let: "v1" := join "handle" in
("v1", "v2").
Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-Notation "e1 ||| e2" := (par (λ: <>, e1)%V (λ: <>, e2)%V) : val_scope.
+Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
Section proof.
Local Set Default Proof Using "Type*".
--
GitLab