Commit cee0b0d8 authored by Robbert Krebbers's avatar Robbert Krebbers

Multi argument recs.

parent ee8c4875
......@@ -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
......@@ -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 :=
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment