chore(*): futureproof import syntax (#2402)

The next community version of Lean will treat a line starting in the first column after an import as a new command, not a continuation of the import.
leanprover-community · Apr 13, 2020 · 64fa9a2 · 64fa9a2
1 parent ef4d235
commit 64fa9a2
Show file tree

Hide file tree

Showing 4 changed files with 4 additions and 4 deletions.
diff --git a/src/analysis/analytic/basic.lean b/src/analysis/analytic/basic.lean
@@ -5,7 +5,7 @@ Authors: Sébastien Gouëzel
 -/
 
 import analysis.calculus.times_cont_diff tactic.omega analysis.complex.exponential
-analysis.specific_limits
+  analysis.specific_limits
 
 /-!
 # Analytic functions

diff --git a/src/topology/metric_space/gromov_hausdorff.lean b/src/topology/metric_space/gromov_hausdorff.lean
@@ -5,7 +5,7 @@ Author: Sébastien Gouëzel
 -/
 
 import topology.metric_space.closeds set_theory.cardinal topology.metric_space.gromov_hausdorff_realized
-topology.metric_space.completion
+  topology.metric_space.completion
 
 /-!
 # Gromov-Hausdorff distance

diff --git a/src/topology/metric_space/gromov_hausdorff_realized.lean b/src/topology/metric_space/gromov_hausdorff_realized.lean
@@ -8,7 +8,7 @@ their Hausdorff distance. This construction is instrumental to study the Gromov-
 distance between nonempty compact metric spaces -/
 
 import topology.bounded_continuous_function topology.metric_space.gluing
-topology.metric_space.hausdorff_distance
+  topology.metric_space.hausdorff_distance
 
 noncomputable theory
 open_locale classical

diff --git a/src/topology/metric_space/isometry.lean b/src/topology/metric_space/isometry.lean
@@ -6,7 +6,7 @@ Authors: Sébastien Gouëzel
 -/
 
 import topology.metric_space.basic
-topology.bounded_continuous_function analysis.normed_space.basic topology.opens
+  topology.bounded_continuous_function analysis.normed_space.basic topology.opens
 
 /-!
 # Isometries