From b0dbc31d4ba05a826c2386fe629cc3b985cd59a4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 16 Aug 2015 18:54:14 -0700
Subject: [PATCH] test(tests/lean/list_vect_numerals): add test mixing
 nat,int,real,list,vector

---
 tests/lean/list_vect_numerals.lean            | 21 +++++++++++++++++++
 .../lean/list_vect_numerals.lean.expected.out |  9 ++++++++
 2 files changed, 30 insertions(+)
 create mode 100644 tests/lean/list_vect_numerals.lean
 create mode 100644 tests/lean/list_vect_numerals.lean.expected.out

diff --git a/tests/lean/list_vect_numerals.lean b/tests/lean/list_vect_numerals.lean
new file mode 100644
index 000000000..167b98cd2
--- /dev/null
+++ b/tests/lean/list_vect_numerals.lean
@@ -0,0 +1,21 @@
+import data.list data.examples.vector data.real
+open nat int real list vector
+
+variables n m : nat
+variables i j : int
+variables x y : real
+variables v   : vector real 3
+
+check [n, m]     -- list nat
+check [n, i]     -- list int
+check [i, n]     -- list int
+check [i, n, x]  -- list real
+
+check ([i, n, x, y] : vector _ _) -- vector of reals
+check (tail [i, n, x, y] = v)
+
+check [i, n, x] = v
+set_option pp.notation false
+set_option pp.full_names true
+check [i, n, x] = v
+check (tail [i, n, x, y] = v)
diff --git a/tests/lean/list_vect_numerals.lean.expected.out b/tests/lean/list_vect_numerals.lean.expected.out
new file mode 100644
index 000000000..b05a60363
--- /dev/null
+++ b/tests/lean/list_vect_numerals.lean.expected.out
@@ -0,0 +1,9 @@
+[n, m] : list ℕ
+[n, i] : list ℤ
+[i, n] : list ℤ
+[i, n, x] : list ℝ
+[i, n, x, y] : vector ℝ 4
+tail [i, n, x, y] = v : Prop
+[i, n, x] = v : Prop
+eq (vector.cons i (vector.cons n (vector.cons x vector.nil))) v : Prop
+eq (vector.tail (vector.cons i (vector.cons n (vector.cons x (vector.cons y vector.nil))))) v : Prop