chore(category): rename to control (#2516)

This is parallel to leanprover-community/lean#202 for community Lean (now merged). It seems the changes are actually completely independent; this compiles against current community Lean, and that PR. (I'm surprised, but I guess it's just that everything is in the root namespace, and in `init/`.) This PR anticipates then renaming `category_theory/` to `category/`. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
leanprover-community · Apr 28, 2020 · d12db89 · d12db89
1 parent c435b1c
commit d12db89
Show file tree

Hide file tree

Showing 35 changed files with 34 additions and 34 deletions.
diff --git a/src/category/traversable/default.lean b/src/category/traversable/default.lean
diff --git a/src/category_theory/core.lean b/src/category_theory/core.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import category_theory.groupoid
-import category.equiv_functor
+import control.equiv_functor
 import category_theory.types
 
 namespace category_theory

diff --git a/src/category/applicative.lean → src/control/applicative.lean b/src/category/applicative.lean → src/control/applicative.lean
@@ -5,7 +5,7 @@ Author: Simon Hudon
 
 Instances for identity and composition functors
 -/
-import category.functor
+import control.functor
 
 universe variables u v w
 

diff --git a/src/category/basic.lean → src/control/basic.lean b/src/category/basic.lean → src/control/basic.lean
diff --git a/src/category/bifunctor.lean → src/control/bifunctor.lean b/src/category/bifunctor.lean → src/control/bifunctor.lean
diff --git a/src/category/bitraversable/basic.lean → src/control/bitraversable/basic.lean b/src/category/bitraversable/basic.lean → src/control/bitraversable/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
-import category.bifunctor
+import control.bifunctor
 
 /-!
 # Bitraversable type class

diff --git a/src/category/bitraversable/instances.lean → src/control/bitraversable/instances.lean b/src/category/bitraversable/instances.lean → src/control/bitraversable/instances.lean
@@ -3,8 +3,8 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Simon Hudon
 -/
-import category.bitraversable.lemmas
-import category.traversable.lemmas
+import control.bitraversable.lemmas
+import control.traversable.lemmas
 
 /-!
 # bitraversable instances

diff --git a/src/category/bitraversable/lemmas.lean → src/control/bitraversable/lemmas.lean b/src/category/bitraversable/lemmas.lean → src/control/bitraversable/lemmas.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Simon Hudon
 -/
-import category.bitraversable.basic
+import control.bitraversable.basic
 
 /-!
 # Bitraversable Lemmas

diff --git a/src/category/equiv_functor.lean → src/control/equiv_functor.lean b/src/category/equiv_functor.lean → src/control/equiv_functor.lean
diff --git a/src/category/equiv_functor/instances.lean → src/control/equiv_functor/instances.lean b/src/category/equiv_functor/instances.lean → src/control/equiv_functor/instances.lean
diff --git a/src/category/fold.lean → src/control/fold.lean b/src/category/fold.lean → src/control/fold.lean
@@ -43,8 +43,8 @@ but the author cannot think of instances of `foldable` that are not also
 -/
 import algebra.free_monoid
 import algebra.opposites
-import category.traversable.instances
-import category.traversable.lemmas
+import control.traversable.instances
+import control.traversable.lemmas
 import category_theory.category
 import category_theory.endomorphism
 import category_theory.types

diff --git a/src/category/functor.lean → src/control/functor.lean b/src/category/functor.lean → src/control/functor.lean
diff --git a/src/category/monad/basic.lean → src/control/monad/basic.lean b/src/category/monad/basic.lean → src/control/monad/basic.lean
diff --git a/src/category/monad/cont.lean → src/control/monad/cont.lean b/src/category/monad/cont.lean → src/control/monad/cont.lean
@@ -7,7 +7,7 @@ Monad encapsulating continuation passing programming style, similar to
 Haskell's `Cont`, `ContT` and `MonadCont`:
 <http://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Cont.html>
 -/
-import category.monad.writer
+import control.monad.writer
 
 universes u v w
 

diff --git a/src/category/monad/writer.lean → src/control/monad/writer.lean b/src/category/monad/writer.lean → src/control/monad/writer.lean
@@ -5,7 +5,7 @@ Authors: Simon Hudon
 
 The writer monad transformer for passing immutable state.
 -/
-import category.monad.basic
+import control.monad.basic
 universes u v w
 
 structure writer_t (ω : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=

diff --git a/src/category/traversable/basic.lean → src/control/traversable/basic.lean b/src/category/traversable/basic.lean → src/control/traversable/basic.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
-import category.applicative
+import control.applicative
 
 /-!
 # Traversable type class

diff --git a/src/control/traversable/default.lean b/src/control/traversable/default.lean
@@ -0,0 +1,2 @@
+import control.traversable.instances
+import control.traversable.lemmas
diff --git a/src/category/traversable/derive.lean → src/control/traversable/derive.lean b/src/category/traversable/derive.lean → src/control/traversable/derive.lean
@@ -5,7 +5,7 @@ Author: Simon Hudon
 
 Automation to construct `traversable` instances
 -/
-import category.traversable.lemmas
+import control.traversable.lemmas
 import data.list.basic
 
 namespace tactic.interactive

diff --git a/src/category/traversable/equiv.lean → src/control/traversable/equiv.lean b/src/category/traversable/equiv.lean → src/control/traversable/equiv.lean
@@ -6,7 +6,7 @@ Authors: Simon Hudon
 Transferring `traversable` instances using isomorphisms.
 -/
 import data.equiv.basic
-import category.traversable.lemmas
+import control.traversable.lemmas
 
 universes u
 

diff --git a/src/category/traversable/instances.lean → src/control/traversable/instances.lean b/src/category/traversable/instances.lean → src/control/traversable/instances.lean
diff --git a/src/category/traversable/lemmas.lean → src/control/traversable/lemmas.lean b/src/category/traversable/lemmas.lean → src/control/traversable/lemmas.lean
@@ -12,7 +12,7 @@ Inspired by:
     In Journal of Functional Programming. Vol. 19. No. 3&4. Pages 377−402. 2009.
     <http://www.cs.ox.ac.uk/jeremy.gibbons/publications/iterator.pdf>
 -/
-import category.traversable.basic
+import control.traversable.basic
 
 universe variables u
 

diff --git a/src/data/array/lemmas.lean b/src/data/array/lemmas.lean
@@ -3,7 +3,7 @@ Copyright (c) 2017 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Mario Carneiro
 -/
-import category.traversable.equiv
+import control.traversable.equiv
 import data.vector2
 
 universes u v w

diff --git a/src/data/buffer/basic.lean b/src/data/buffer/basic.lean
@@ -7,7 +7,7 @@ Traversable instance for buffers.
 -/
 import data.buffer
 import data.array.lemmas
-import category.traversable.instances
+import control.traversable.instances
 
 namespace buffer
 

diff --git a/src/data/dlist/instances.lean b/src/data/dlist/instances.lean
@@ -6,8 +6,8 @@ Authors: Simon Hudon
 Traversable instance for dlists.
 -/
 import data.dlist
-import category.traversable.equiv
-import category.traversable.instances
+import control.traversable.equiv
+import control.traversable.instances
 
 namespace dlist
 

diff --git a/src/data/equiv/functor.lean b/src/data/equiv/functor.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin, Simon Hudon, Scott Morrison
 -/
 import data.equiv.basic
-import category.bifunctor
+import control.bifunctor
 
 /-!
 # Functor and bifunctors can be applied to `equiv`s.

diff --git a/src/data/fin_enum.lean b/src/data/fin_enum.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author(s): Simon Hudon
 -/
-import category.monad.basic
+import control.monad.basic
 import data.fintype.basic
 
 /-!

diff --git a/src/data/lazy_list2.lean b/src/data/lazy_list2.lean
@@ -5,8 +5,8 @@ Authors: Simon Hudon
 
 Traversable instance for lazy_lists.
 -/
-import category.traversable.equiv
-import category.traversable.instances
+import control.traversable.equiv
+import control.traversable.instances
 import data.lazy_list
 
 universes u

diff --git a/src/data/multiset.lean b/src/data/multiset.lean
@@ -10,8 +10,8 @@ import data.list.intervals
 import data.list.antidiagonal
 import data.string.basic
 import algebra.group_power
-import category.traversable.lemmas
-import category.traversable.instances
+import control.traversable.lemmas
+import control.traversable.instances
 
 open list subtype nat
 

diff --git a/src/tactic/converter/old_conv.lean b/src/tactic/converter/old_conv.lean
@@ -5,7 +5,7 @@ Authors: Leonardo de Moura
 
 Converter monad for building simplifiers.
 -/
-import category.basic
+import control.basic
 open tactic
 
 meta structure old_conv_result (α : Type) :=

diff --git a/src/tactic/core.lean b/src/tactic/core.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Simon Hudon, Scott Morrison, Keeley Hoek
 -/
 import data.dlist.basic
-import category.basic
+import control.basic
 import meta.expr
 import meta.rb_map
 import data.bool

diff --git a/src/tactic/equiv_rw.lean b/src/tactic/equiv_rw.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
-import category.equiv_functor
+import control.equiv_functor
 
 /-!
 # The `equiv_rw` tactic transports goals or hypotheses along equivalences.

diff --git a/src/tactic/monotonicity/interactive.lean b/src/tactic/monotonicity/interactive.lean
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
 import tactic.monotonicity.basic
-import category.traversable
-import category.traversable.derive
+import control.traversable
+import control.traversable.derive
 import data.dlist
 
 variables {a b c p : Prop}

diff --git a/src/tactic/squeeze.lean b/src/tactic/squeeze.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Simon Hudon. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Simon Hudon
 -/
-import category.traversable.basic
+import control.traversable.basic
 import tactic.simpa
 
 open interactive interactive.types lean.parser

diff --git a/test/equiv_rw.lean b/test/equiv_rw.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison
 -/
 import tactic.equiv_rw
-import category.equiv_functor.instances -- these make equiv_rw more powerful!
+import control.equiv_functor.instances -- these make equiv_rw more powerful!
 
 -- Uncomment this line to observe the steps of constructing appropriate equivalences.
 -- set_option trace.equiv_rw_type true

diff --git a/test/traversable.lean b/test/traversable.lean
@@ -1,4 +1,4 @@
-import category.traversable.derive
+import control.traversable.derive
 import tactic
 
 universes u