refactor(library/data): move vector as indexed family to examples folder

doc/lean/declarations.org

@@ -16,9 +16,9 @@ the expression =v = w= since it would not be able to establish that
 _definitionally equal_.
 
 #+BEGIN_SRC lean
-  import data.vector data.nat
+  import data.fixed_list data.nat
   open nat
-  check λ (v : vector nat (2+3)) (w : vector nat 5), v = w
+  check λ (v : fixed_list nat (2+3)) (w : fixed_list nat 5), v = w
 #+END_SRC
 
 Similarly, the following definition only type checks because =id= is transparent, and the type checker can establish that

library/data/default.lean

@@ -4,4 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Jeremy Avigad
 -/
 import .empty .unit .bool .num .string .nat .int .rat .fintype
-import .prod .sum .sigma .option .subtype .quotient .list .vector .finset .set .stream
+import .prod .sum .sigma .option .subtype .quotient .list .finset .set .stream
+import .fin

library/data/examples/vector.lean

@@ -2,8 +2,11 @@
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Floris van Doorn, Leonardo de Moura
+
+This file demonstrates how to encode vectors using indexed inductive families.
+In standard library we do not use this approach.
 -/
-import data.nat data.list data.fin
+import data.nat data.list data.fin data.fixed_list
 open nat prod fin
 
 inductive vector (A : Type) : nat → Type :=

tests/lean/extra/rec.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 definition fib : nat → nat,

tests/lean/extra/rec4.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 set_option pp.implicit true

tests/lean/gen_fail.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat
 
 theorem tst (n : nat) (v : vector nat n) : v = v :=

tests/lean/nonexhaustive.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 variable {A : Type}

tests/lean/revert_fail.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 
 example (A : Type) (n : nat) (v : vector A n) : v = v :=
 begin

tests/lean/run/682.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat prod.ops
 
 example (n : nat) (v₁ : vector nat n) (v₂ : vector nat 0) (h₁ : (v₂, n).2 = 0) (h₂ : n = 0) (h₃ : eq.rec_on h₁ v₁ = v₂) : v₂ = eq.rec_on h₂ v₁ :=

tests/lean/run/deceq_vec.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open vector nat decidable
 
 variable A : Type

tests/lean/run/dfun_tst.lean

@@ -1,4 +1,4 @@
-import logic data.prod data.vector
+import logic data.prod data.examples.vector
 open prod nat inhabited vector
 
 theorem tst1 : inhabited (vector nat 2)

tests/lean/run/diag.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat
 
 namespace vector

tests/lean/run/eq18.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 definition last {A : Type} : Π {n}, vector A (succ n) → A

tests/lean/run/eq19.lean

@@ -1,4 +1,4 @@
-import data.vector data.prod
+import data.examples.vector data.prod
 open nat vector prod
 
 variables {A B : Type}

tests/lean/run/eq3.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 definition swap {A : Type} : Π {n}, vector A (succ (succ n)) → vector A (succ (succ n))

tests/lean/run/eq7.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 definition diag {A : Type} : Π {n}, vector (vector A n) n → vector A n

tests/lean/run/eq8.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open vector
 
 definition map {A B C : Type} (f : A → B → C) : Π {n}, vector A n → vector B n → vector C n

tests/lean/run/induction_tac1.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open vector
 
 set_option pp.implicit true

tests/lean/run/inj_tac.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 example (a b : nat) : succ a = succ b → a + 2 = b + 2 :=

tests/lean/run/inv_bug2.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat
 
 namespace vector

tests/lean/run/unfold_rec.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 variables {A B : Type}

tests/lean/run/unfold_rec2.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 variable {A : Type}

tests/lean/run/unfold_test.lean

@@ -1,4 +1,4 @@
-import data.list data.vector
+import data.list data.examples.vector
 
 variables {A B : Type}
 

tests/lean/run/unzip_bug.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector prod
 
 variables {A B : Type}

tests/lean/unfold_rec.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector
 
 variables {A B : Type}

tests/lean/unzip_error.lean

@@ -1,4 +1,4 @@
-import data.vector
+import data.examples.vector
 open nat vector prod
 
 variables {A B : Type}

tests/lean/urec.lean

@@ -1,4 +1,4 @@
-import data.nat data.vector data.list.basic
+import data.nat data.examples.vector data.list.basic
 
 attribute nat [recursor]