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)