refactor(category_theory/instances): rename examples to instances

leanprover-community · Jan 30, 2019 · 12be0aa · 12be0aa
1 parent 829b49b
commit 12be0aa
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 11 deletions.
diff --git a/...ory_theory/examples/measurable_space.lean → ...ry_theory/instances/measurable_space.lean b/...ory_theory/examples/measurable_space.lean → ...ry_theory/instances/measurable_space.lean
@@ -5,13 +5,13 @@ Authors: Johannes Hölzl
 Basic setup for measurable spaces.
 -/
 
-import category_theory.examples.topological_spaces
+import category_theory.instances.topological_spaces
 import measure_theory.borel_space
 
 open category_theory
 universes u v
 
-namespace category_theory.examples
+namespace category_theory.instances
 
 @[reducible] def Meas : Type (u+1) := bundled measurable_space
 
@@ -29,4 +29,4 @@ end Meas
 def Borel : Top ⥤ Meas :=
 concrete_functor @measure_theory.borel @measure_theory.measurable_of_continuous
 
-end category_theory.examples
+end category_theory.instances
diff --git a/src/category_theory/examples/monoids.lean → src/category_theory/instances/monoids.lean b/src/category_theory/examples/monoids.lean → src/category_theory/instances/monoids.lean
@@ -16,7 +16,7 @@ universes u v
 
 open category_theory
 
-namespace category_theory.examples
+namespace category_theory.instances
 
 /-- The category of monoids and monoid morphisms. -/
 @[reducible] def Mon : Type (u+1) := bundled monoid
@@ -55,4 +55,4 @@ instance : faithful (forget_to_Mon) := {}
 
 end CommMon
 
-end category_theory.examples
+end category_theory.instances
diff --git a/src/category_theory/examples/rings.lean → src/category_theory/instances/rings.lean b/src/category_theory/examples/rings.lean → src/category_theory/instances/rings.lean
@@ -8,7 +8,7 @@ Currently only the basic setup.
 -/
 
 import category_theory.concrete_category
-import category_theory.examples.monoids
+import category_theory.instances.monoids
 import category_theory.fully_faithful
 import category_theory.adjunction
 import linear_algebra.multivariate_polynomial
@@ -18,7 +18,7 @@ universes u v
 
 open category_theory
 
-namespace category_theory.examples
+namespace category_theory.instances
 
 /-- The category of rings. -/
 @[reducible] def Ring : Type (u+1) := bundled ring
@@ -138,4 +138,4 @@ end
 
 end CommRing
 
-end category_theory.examples
+end category_theory.instances
diff --git a/...y_theory/examples/topological_spaces.lean → ..._theory/instances/topological_spaces.lean b/...y_theory/examples/topological_spaces.lean → ..._theory/instances/topological_spaces.lean
@@ -19,7 +19,7 @@ open topological_space
 
 universe u
 
-namespace category_theory.examples
+namespace category_theory.instances
 
 /-- The category of topological spaces and continuous maps. -/
 @[reducible] def Top : Type (u+1) := bundled topological_space
@@ -110,9 +110,9 @@ instance : small_category (opens X) := by apply_instance
 def nbhd (x : X.α) := { U : opens X // x ∈ U }
 def nbhds (x : X.α) : small_category (nbhd x) := begin unfold nbhd, apply_instance end
 
-end category_theory.examples
+end category_theory.instances
 
-open category_theory.examples
+open category_theory.instances
 
 namespace topological_space.opens