From 7d4fe55bffdb972cb352de4cede620d673632d3c Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Thu, 20 Jul 2017 23:19:02 +0100
Subject: [PATCH] fix(tests/lean/run/choice_anon_ctor): fix test

---
 tests/lean/run/choice_anon_ctor.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/tests/lean/run/choice_anon_ctor.lean b/tests/lean/run/choice_anon_ctor.lean
index b2f72866ad..36d3282f68 100644
--- a/tests/lean/run/choice_anon_ctor.lean
+++ b/tests/lean/run/choice_anon_ctor.lean
@@ -1,4 +1,9 @@
-import data.list data.vector
+constant vector : Type → nat → Type
+constant vector.nil {α} : vector α 0
+constant vector.cons {α n} : α → vector α n → vector α (nat.succ n)
+
+notation a :: b := vector.cons a b
+notation `[` l:(foldr `, ` (h t, vector.cons h t) vector.nil `]`) := l
 
 structure author :=
 (name : string)