From 1b6e40d3d64cf472e8f2b8d7f70ea93ad184353a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 8 Nov 2014 20:11:46 -0800
Subject: [PATCH] test(tests/lean/run): define below_rec_on (aka brec_on) for
 vectors

---
 tests/lean/run/vector.lean | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 4a2e0d93fc..3c69198448 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -1,5 +1,5 @@
-import logic data.nat.basic
-open nat
+import logic data.nat.basic data.prod data.unit
+open nat prod
 
 inductive vector (A : Type) : nat → Type :=
 vnil  : vector A zero,
@@ -17,4 +17,32 @@ namespace vector
   begin
      intro h, apply heq.to_eq, apply (no_confusion h), intros, eassumption,
   end
+
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable C : Π (n : nat), vector A n → Type.{l₂}
+    definition below {n : nat} (v : vector A n) :=
+    rec_on v unit.{max 1 l₂} (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : Type.{max 1 l₂}), C n₁ v₁ × r₁)
+  end
+
+  section
+    universe variables l₁ l₂
+    variable {A : Type.{l₁}}
+    variable {C : Π (n : nat), vector A n → Type.{l₂}}
+    definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), below C v → C n v) : C n v :=
+    have general : C n v × below C v, from
+      rec_on v
+       (pair (H zero (vnil A) unit.star) unit.star)
+       (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × below C v₁),
+          have b : below C (vcons a₁ v₁), from
+            r₁,
+          have c : C (succ n₁) (vcons a₁ v₁), from
+            H (succ n₁) (vcons a₁ v₁) b,
+          pair c b),
+    pr₁ general
+  end
+
+  check brec_on
+
 end vector