From b4024982a2c10773d3be17533dd701d7073e3b70 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Aug 2015 15:05:14 -0700 Subject: [PATCH] refactor(library/data): move vector as indexed family to examples folder --- doc/lean/declarations.org | 4 ++-- library/data/default.lean | 3 ++- library/data/{ => examples}/vector.lean | 5 ++++- tests/lean/extra/rec.lean | 2 +- tests/lean/extra/rec4.lean | 2 +- tests/lean/gen_fail.lean | 2 +- tests/lean/nonexhaustive.lean | 2 +- tests/lean/revert_fail.lean | 2 +- tests/lean/run/682.lean | 2 +- tests/lean/run/deceq_vec.lean | 2 +- tests/lean/run/dfun_tst.lean | 2 +- tests/lean/run/diag.lean | 2 +- tests/lean/run/eq18.lean | 2 +- tests/lean/run/eq19.lean | 2 +- tests/lean/run/eq3.lean | 2 +- tests/lean/run/eq7.lean | 2 +- tests/lean/run/eq8.lean | 2 +- tests/lean/run/induction_tac1.lean | 2 +- tests/lean/run/inj_tac.lean | 2 +- tests/lean/run/inv_bug2.lean | 2 +- tests/lean/run/unfold_rec.lean | 2 +- tests/lean/run/unfold_rec2.lean | 2 +- tests/lean/run/unfold_test.lean | 2 +- tests/lean/run/unzip_bug.lean | 2 +- tests/lean/unfold_rec.lean | 2 +- tests/lean/unzip_error.lean | 2 +- tests/lean/urec.lean | 2 +- 27 files changed, 32 insertions(+), 28 deletions(-) rename library/data/{ => examples}/vector.lean (98%) diff --git a/doc/lean/declarations.org b/doc/lean/declarations.org index 78078962d..109388223 100644 --- a/doc/lean/declarations.org +++ b/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 diff --git a/library/data/default.lean b/library/data/default.lean index 77b3e597e..bdf9387f5 100644 --- a/library/data/default.lean +++ b/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 diff --git a/library/data/vector.lean b/library/data/examples/vector.lean similarity index 98% rename from library/data/vector.lean rename to library/data/examples/vector.lean index 7b929a28f..7b3d95cd7 100644 --- a/library/data/vector.lean +++ b/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 := diff --git a/tests/lean/extra/rec.lean b/tests/lean/extra/rec.lean index 5bd465439..07373f1a5 100644 --- a/tests/lean/extra/rec.lean +++ b/tests/lean/extra/rec.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector definition fib : nat → nat, diff --git a/tests/lean/extra/rec4.lean b/tests/lean/extra/rec4.lean index e09cc508f..eef6d94eb 100644 --- a/tests/lean/extra/rec4.lean +++ b/tests/lean/extra/rec4.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector set_option pp.implicit true diff --git a/tests/lean/gen_fail.lean b/tests/lean/gen_fail.lean index c0bb80a62..1cfe57781 100644 --- a/tests/lean/gen_fail.lean +++ b/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 := diff --git a/tests/lean/nonexhaustive.lean b/tests/lean/nonexhaustive.lean index 9a83af941..0fea2f385 100644 --- a/tests/lean/nonexhaustive.lean +++ b/tests/lean/nonexhaustive.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector variable {A : Type} diff --git a/tests/lean/revert_fail.lean b/tests/lean/revert_fail.lean index 09905ee7e..33b635f44 100644 --- a/tests/lean/revert_fail.lean +++ b/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 diff --git a/tests/lean/run/682.lean b/tests/lean/run/682.lean index 7ee337bfa..5ebd62f4b 100644 --- a/tests/lean/run/682.lean +++ b/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₁ := diff --git a/tests/lean/run/deceq_vec.lean b/tests/lean/run/deceq_vec.lean index 4f7f9555a..bc9f46f29 100644 --- a/tests/lean/run/deceq_vec.lean +++ b/tests/lean/run/deceq_vec.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open vector nat decidable variable A : Type diff --git a/tests/lean/run/dfun_tst.lean b/tests/lean/run/dfun_tst.lean index ffb5f777b..b9e87cc80 100644 --- a/tests/lean/run/dfun_tst.lean +++ b/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) diff --git a/tests/lean/run/diag.lean b/tests/lean/run/diag.lean index af5f8856d..628d3c16a 100644 --- a/tests/lean/run/diag.lean +++ b/tests/lean/run/diag.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat namespace vector diff --git a/tests/lean/run/eq18.lean b/tests/lean/run/eq18.lean index 1073158ef..c0b963742 100644 --- a/tests/lean/run/eq18.lean +++ b/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 diff --git a/tests/lean/run/eq19.lean b/tests/lean/run/eq19.lean index d695c6903..f307ab106 100644 --- a/tests/lean/run/eq19.lean +++ b/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} diff --git a/tests/lean/run/eq3.lean b/tests/lean/run/eq3.lean index b281d7290..e773d9be8 100644 --- a/tests/lean/run/eq3.lean +++ b/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)) diff --git a/tests/lean/run/eq7.lean b/tests/lean/run/eq7.lean index aa20d9189..176fb3508 100644 --- a/tests/lean/run/eq7.lean +++ b/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 diff --git a/tests/lean/run/eq8.lean b/tests/lean/run/eq8.lean index 3f4d99aca..53c368cf5 100644 --- a/tests/lean/run/eq8.lean +++ b/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 diff --git a/tests/lean/run/induction_tac1.lean b/tests/lean/run/induction_tac1.lean index fb305ad4e..eb16fca51 100644 --- a/tests/lean/run/induction_tac1.lean +++ b/tests/lean/run/induction_tac1.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open vector set_option pp.implicit true diff --git a/tests/lean/run/inj_tac.lean b/tests/lean/run/inj_tac.lean index d85ed066d..6d6bdb19e 100644 --- a/tests/lean/run/inj_tac.lean +++ b/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 := diff --git a/tests/lean/run/inv_bug2.lean b/tests/lean/run/inv_bug2.lean index 400c13265..66ee2c97c 100644 --- a/tests/lean/run/inv_bug2.lean +++ b/tests/lean/run/inv_bug2.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat namespace vector diff --git a/tests/lean/run/unfold_rec.lean b/tests/lean/run/unfold_rec.lean index a19b624eb..4cba6a278 100644 --- a/tests/lean/run/unfold_rec.lean +++ b/tests/lean/run/unfold_rec.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector variables {A B : Type} diff --git a/tests/lean/run/unfold_rec2.lean b/tests/lean/run/unfold_rec2.lean index ded9d3afc..4f601b92d 100644 --- a/tests/lean/run/unfold_rec2.lean +++ b/tests/lean/run/unfold_rec2.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector variable {A : Type} diff --git a/tests/lean/run/unfold_test.lean b/tests/lean/run/unfold_test.lean index 2b0fa77de..73fb33d92 100644 --- a/tests/lean/run/unfold_test.lean +++ b/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} diff --git a/tests/lean/run/unzip_bug.lean b/tests/lean/run/unzip_bug.lean index c71656dc5..f5fcad27b 100644 --- a/tests/lean/run/unzip_bug.lean +++ b/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} diff --git a/tests/lean/unfold_rec.lean b/tests/lean/unfold_rec.lean index a19b624eb..4cba6a278 100644 --- a/tests/lean/unfold_rec.lean +++ b/tests/lean/unfold_rec.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector variables {A B : Type} diff --git a/tests/lean/unzip_error.lean b/tests/lean/unzip_error.lean index 6cd44ffcd..25fb95ce2 100644 --- a/tests/lean/unzip_error.lean +++ b/tests/lean/unzip_error.lean @@ -1,4 +1,4 @@ -import data.vector +import data.examples.vector open nat vector prod variables {A B : Type} diff --git a/tests/lean/urec.lean b/tests/lean/urec.lean index a378b947d..bc040f07d 100644 --- a/tests/lean/urec.lean +++ b/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]