test(tests/lean/list_vect_numerals): add test mixing nat,int,real,list,vector

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)

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