From cee0b0d868c0a45108060bb9c1b911e8c075ad32 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 12 Feb 2016 00:55:28 +0100
Subject: [PATCH] Multi argument recs.

---
 heap_lang/notation.v | 9 +++++++++
 heap_lang/tests.v    | 2 +-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index fc50c8095..7a266d155 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -54,3 +54,12 @@ Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
   (at level 102, x at level 1, e1, e2 at level 200) : lang_scope.
 Notation "e1 ;; e2" := (Lam "" e2%L e1%L)
   (at level 100, e2 at level 200) : lang_scope.
+
+Notation "'rec:' f x y := e" := (Rec f x (Lam y e%L))
+  (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
+Notation "'rec:' f x y := e" := (RecV f x (Lam y e%L))
+  (at level 102, f, x, y at level 1, e at level 200) : lang_scope.
+Notation "'rec:' f x y z := e" := (Rec f x (Lam y (Lam z e%L)))
+  (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
+Notation "'rec:' f x y z := e" := (RecV f x (Lam y (Lam z e%L)))
+  (at level 102, f, x, y, z at level 1, e at level 200) : lang_scope.
\ No newline at end of file
diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index 1abdf6265..8c1e941a0 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -55,7 +55,7 @@ Module LiftingTests.
   Qed.
 
   Definition FindPred : val :=
-    rec: "pred" "x" := λ: "y", 
+    rec: "pred" "x" "y" :=
       let: "yp" := "y" + '1 in
       if "yp" < "x" then "pred" "x" "yp" else "y".
   Definition Pred : val :=
-- 
GitLab