chore: fix imports using script

This is just a draft.
```
for f in `find . -name '*.lean'`; do echo $f; gsed "/^import/s/\b\(.\)/\u\1/g" $f > tmp; gsed "/^Import/s/Import/import/g" tmp > $f; done
```

library/Init/Coe.lean

@@ -24,7 +24,7 @@ We use the HasCoeToSort type class for encoding coercions from
 a Type to a sort.
 -/
 prelude
-import init.data.list.basic
+import Init.Data.List.Basic
 universes u v
 
 class HasLift (a : Sort u) (b : Sort v) :=

library/Init/Control/Alternative.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.core
-import init.control.applicative
+import Init.Core
+import Init.Control.Applicative
 universes u v
 
 class Alternative (f : Type u → Type v) extends Applicative f : Type (max (u+1) v) :=

library/Init/Control/Applicative.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.control.functor
+import Init.Control.Functor
 open Function
 universes u v
 

library/Init/Control/Combinators.lean

@@ -6,9 +6,9 @@ Authors: Jeremy Avigad, Leonardo de Moura
 Monad Combinators, as in Haskell's Control.Monad.
 -/
 prelude
-import init.control.monad
-import init.control.alternative
-import init.data.list.basic
+import Init.Control.Monad
+import Init.Control.Alternative
+import Init.Data.List.Basic
 
 universes u v w u₁ u₂ u₃
 

library/Init/Control/Conditional.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.control.monad
-import init.data.option.basic
+import Init.Control.Monad
+import Init.Data.Option.Basic
 universes u v
 
 class HasToBool (α : Type u) :=

library/Init/Control/Default.lean

@@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.applicative
-import init.control.functor
-import init.control.alternative
-import init.control.monad
-import init.control.lift
-import init.control.state
-import init.control.id
-import init.control.except
-import init.control.reader
-import init.control.option
-import init.control.combinators
-import init.control.conditional
+import Init.Control.Applicative
+import Init.Control.Functor
+import Init.Control.Alternative
+import Init.Control.Monad
+import Init.Control.Lift
+import Init.Control.State
+import Init.Control.Id
+import Init.Control.Except
+import Init.Control.Reader
+import Init.Control.Option
+import Init.Control.Combinators
+import Init.Control.Conditional

library/Init/Control/Estate.lean

@@ -8,8 +8,8 @@ of memory allocations using the approach described in the paper
 "Counting immutable beans" by Sebastian and Leo
 -/
 prelude
-import init.control.state
-import init.control.except
+import Init.Control.State
+import Init.Control.Except
 universes u v
 
 namespace EState

library/Init/Control/Except.lean

@@ -6,10 +6,10 @@ Authors: Jared Roesch, Sebastian Ullrich
 The Except monad transformer.
 -/
 prelude
-import init.control.alternative
-import init.control.lift
-import init.data.tostring
-import init.control.monadfail
+import Init.Control.Alternative
+import Init.Control.Lift
+import Init.Data.Tostring
+import Init.Control.Monadfail
 universes u v w
 
 inductive Except (ε : Type u) (α : Type v)

library/Init/Control/Functor.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Luke Nelson, Jared Roesch, Sebastian Ullrich, Leonardo de Moura
 -/
 prelude
-import init.core
+import Init.Core
 open Function
 universes u v
 

library/Init/Control/Id.lean

@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich
 The identity Monad.
 -/
 prelude
-import init.control.lift
+import Init.Control.Lift
 universe u
 
 def Id (type : Type u) : Type u := type

library/Init/Control/Lift.lean

@@ -9,8 +9,8 @@ This theory is roughly modeled after the Haskell 'layers' package https://hackag
 Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html for an exhaustive discussion of the different approaches to lift functions.
 -/
 prelude
-import init.coe
-import init.control.monad
+import Init.Coe
+import Init.Control.Monad
 
 universes u v w
 

library/Init/Control/Monad.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Luke Nelson, Jared Roesch, Sebastian Ullrich
 -/
 prelude
-import init.control.applicative
+import Init.Control.Applicative
 universes u v w
 
 open Function

library/Init/Control/Monadfail.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.lift
-import init.data.string.basic
+import Init.Control.Lift
+import Init.Data.String.Basic
 
 universes u v
 

library/Init/Control/Option.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 prelude
-import init.control.alternative
-import init.control.lift
-import init.control.except
+import Init.Control.Alternative
+import Init.Control.Lift
+import Init.Control.Except
 
 universes u v
 

library/Init/Control/Reader.lean

@@ -7,10 +7,10 @@ The Reader monad transformer for passing immutable State.
 -/
 
 prelude
-import init.control.lift
-import init.control.id
-import init.control.alternative
-import init.control.except
+import Init.Control.Lift
+import Init.Control.Id
+import Init.Control.Alternative
+import Init.Control.Except
 universes u v w
 
 /-- An implementation of [ReaderT](https://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-Reader.html#t:ReaderT) -/

library/Init/Control/State.lean

@@ -6,10 +6,10 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 The State monad transformer.
 -/
 prelude
-import init.control.alternative
-import init.control.lift
-import init.control.id
-import init.control.except
+import Init.Control.Alternative
+import Init.Control.Lift
+import Init.Control.Id
+import Init.Control.Except
 universes u v w
 
 def StateT (σ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=

library/Init/Data/Array/Basic.lean

@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic
-import init.data.fin.basic
-import init.data.uint
-import init.data.repr
-import init.data.tostring
-import init.control.id
-import init.util
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.Uint
+import Init.Data.Repr
+import Init.Data.Tostring
+import Init.Control.Id
+import Init.Util
 universes u v w
 
 /-

library/Init/Data/Array/BinSearch.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.array.basic
+import Init.Data.Array.Basic
 universes u v
 
 namespace Array

library/Init/Data/Array/Default.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Gabriel Ebner
 -/
 prelude
-import init.data.array.basic
-import init.data.array.qsort
-import init.data.array.binsearch
+import Init.Data.Array.Basic
+import Init.Data.Array.Qsort
+import Init.Data.Array.Binsearch

library/Init/Data/Array/QSort.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.array.basic
+import Init.Data.Array.Basic
 
 namespace Array
 -- TODO: remove the [Inhabited α] parameters as soon as we have the tactic framework for automating proof generation and using Array.fget

library/Init/Data/AssocList.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.control.id
+import Init.Control.Id
 universes u v w
 
 /- List-like type to avoid extra level of indirection -/

library/Init/Data/Basic.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic
-import init.data.fin.basic
-import init.data.list.basic
-import init.data.char.basic
-import init.data.string.basic
-import init.data.option.basic
-import init.data.uint
-import init.data.repr
-import init.data.tostring
+import Init.Data.Nat.Basic
+import Init.Data.Fin.Basic
+import Init.Data.List.Basic
+import Init.Data.Char.Basic
+import Init.Data.String.Basic
+import Init.Data.Option.Basic
+import Init.Data.Uint
+import Init.Data.Repr
+import Init.Data.Tostring

library/Init/Data/BinomialHeap/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.list
-import init.coe
+import Init.Data.List
+import Init.Coe
 universes u
 
 namespace BinomialHeapImp

library/Init/Data/BinomialHeap/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.binomialheap.basic
+import Init.Data.Binomialheap.Basic

library/Init/Data/ByteArray/Basic.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.array.basic
-import init.data.uint
-import init.data.option.basic
+import Init.Data.Array.Basic
+import Init.Data.Uint
+import Init.Data.Option.Basic
 universes u
 
 structure ByteArray :=

library/Init/Data/ByteArray/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.bytearray.basic
+import Init.Data.Bytearray.Basic

library/Init/Data/Char/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.uint
+import Init.Data.Uint
 @[inline, reducible] def isValidChar (n : UInt32) : Prop :=
 n < 0xd800 ∨ (0xdfff < n ∧ n < 0x110000)
 

library/Init/Data/Char/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.char.basic
+import Init.Data.Char.Basic

library/Init/Data/DList.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic
+import Init.Data.List.Basic
 universes u
 /--
 A difference List is a Function that, given a List, returns the original

library/Init/Data/Default.lean

@@ -4,19 +4,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.basic
-import init.data.nat
-import init.data.char
-import init.data.string
-import init.data.list
-import init.data.int
-import init.data.array
-import init.data.bytearray
-import init.data.fin
-import init.data.uint
-import init.data.rbtree
-import init.data.rbmap
-import init.data.option
-import init.data.hashmap
-import init.data.random
-import init.data.queue
+import Init.Data.Basic
+import Init.Data.Nat
+import Init.Data.Char
+import Init.Data.String
+import Init.Data.List
+import Init.Data.Int
+import Init.Data.Array
+import Init.Data.Bytearray
+import Init.Data.Fin
+import Init.Data.Uint
+import Init.Data.Rbtree
+import Init.Data.Rbmap
+import Init.Data.Option
+import Init.Data.Hashmap
+import Init.Data.Random
+import Init.Data.Queue

library/Init/Data/Fin/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.nat.div
-import init.data.nat.bitwise
+import Init.Data.Nat.Div
+import Init.Data.Nat.Bitwise
 
 open Nat
 structure Fin (n : Nat) := (val : Nat) (isLt : val < n)

library/Init/Data/Fin/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.fin.basic
+import Init.Data.Fin.Basic

library/Init/Data/HashMap/Basic.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.array.basic
-import init.data.assoclist
-import init.data.option.basic
-import init.data.hashable
+import Init.Data.Array.Basic
+import Init.Data.Assoclist
+import Init.Data.Option.Basic
+import Init.Data.Hashable
 universes u v w
 
 def HashMapBucket (α : Type u) (β : Type v) :=

library/Init/Data/HashMap/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.hashmap.basic
+import Init.Data.Hashmap.Basic

library/Init/Data/Hashable.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.uint
-import init.data.string
+import Init.Data.Uint
+import Init.Data.String
 universes u
 
 class Hashable (α : Type u) :=

library/Init/Data/Int/Basic.lean

@@ -6,11 +6,11 @@ Authors: Jeremy Avigad, Leonardo de Moura
 The integers, with addition, multiplication, and subtraction.
 -/
 prelude
-import init.data.nat.basic
-import init.data.list
-import init.coe
-import init.data.repr
-import init.data.tostring
+import Init.Data.Nat.Basic
+import Init.Data.List
+import Init.Coe
+import Init.Data.Repr
+import Init.Data.Tostring
 open Nat
 
 /- the Type, coercions, and notation -/

library/Init/Data/Int/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.int.basic
+import Init.Data.Int.Basic

library/Init/Data/List/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.core
-import init.data.nat.basic
+import Init.Core
+import Init.Data.Nat.Basic
 open Decidable List
 
 universes u v w

library/Init/Data/List/BasicAux.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic
-import init.util
+import Init.Data.List.Basic
+import Init.Util
 
 universes u
 

library/Init/Data/List/Default.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic
-import init.data.list.basicaux
-import init.data.list.instances
+import Init.Data.List.Basic
+import Init.Data.List.Basicaux
+import Init.Data.List.Instances

library/Init/Data/List/Instances.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic
-import init.control.alternative
-import init.control.monad
+import Init.Data.List.Basic
+import Init.Control.Alternative
+import Init.Control.Monad
 open List
 
 universes u v

library/Init/Data/Nat/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Floris van Doorn, Leonardo de Moura
 -/
 prelude
-import init.core
+import Init.Core
 universes u
 
 namespace Nat

library/Init/Data/Nat/Bitwise.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic
-import init.data.nat.div
-import init.coe
+import Init.Data.Nat.Basic
+import Init.Data.Nat.Div
+import Init.Coe
 
 namespace Nat
 

library/Init/Data/Nat/Default.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.nat.basic
-import init.data.nat.div
-import init.data.nat.bitwise
+import Init.Data.Nat.Basic
+import Init.Data.Nat.Div
+import Init.Data.Nat.Bitwise

library/Init/Data/Nat/Div.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.wf
-import init.data.nat.basic
+import Init.Wf
+import Init.Data.Nat.Basic
 namespace Nat
 
 private def divRecLemma {x y : Nat} : 0 < y ∧ y ≤ x → x - y < x :=

library/Init/Data/Option/Basic.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.core
-import init.control.monad
-import init.control.alternative
-import init.coe
+import Init.Core
+import Init.Control.Monad
+import Init.Control.Alternative
+import Init.Coe
 open Decidable
 
 universes u v

library/Init/Data/Option/BasicAux.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.option.basic
-import init.util
+import Init.Data.Option.Basic
+import Init.Util
 
 universes u
 

library/Init/Data/Option/Default.lean

@@ -4,6 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.option.basic
-import init.data.option.basicaux
-import init.data.option.instances
+import Init.Data.Option.Basic
+import Init.Data.Option.Basicaux
+import Init.Data.Option.Instances

library/Init/Data/Option/Instances.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.option.basic
+import Init.Data.Option.Basic
 
 universes u v
 

library/Init/Data/PersistentArray/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.array
+import Init.Data.Array
 universes u v w
 
 inductive PersistentArrayNode (α : Type u)

library/Init/Data/PersistentArray/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.persistentarray.basic
+import Init.Data.Persistentarray.Basic

library/Init/Data/PersistentHashMap/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.array
-import init.data.hashable
+import Init.Data.Array
+import Init.Data.Hashable
 universes u v w w'
 
 namespace PersistentHashMap

library/Init/Data/PersistentHashMap/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.persistenthashmap.basic
+import Init.Data.Persistenthashmap.Basic

library/Init/Data/Queue/Basic.lean

@@ -7,8 +7,8 @@ Simple queue implemented using two lists.
 Note: this is only a temporary placeholder.
 -/
 prelude
-import init.data.array
-import init.data.int
+import Init.Data.Array
+import Init.Data.Int
 universes u v w
 
 structure Queue (α : Type u) :=

library/Init/Data/Queue/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Daniel Selsam
 -/
 prelude
-import init.data.queue.basic
+import Init.Data.Queue.Basic

library/Init/Data/RBMap/Basic.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.repr
-import init.data.option.basic
+import Init.Data.Repr
+import Init.Data.Option.Basic
 
 universes u v w w'
 

library/Init/Data/RBMap/BasicAux.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbmap.basic
-import init.util
+import Init.Data.Rbmap.Basic
+import Init.Util
 
 universes u v w w'
 

library/Init/Data/RBMap/Default.lean

@@ -4,5 +4,5 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbmap.basic
-import init.data.rbmap.basicaux
+import Init.Data.Rbmap.Basic
+import Init.Data.Rbmap.Basicaux

library/Init/Data/RBTree/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbmap.basic
+import Init.Data.Rbmap.Basic
 universes u v w
 
 def RBTree (α : Type u) (lt : α → α → Bool) : Type u :=

library/Init/Data/RBTree/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.rbtree.basic
+import Init.Data.Rbtree.Basic

library/Init/Data/Random.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.system.io
-import init.data.int
+import Init.System.Io
+import Init.Data.Int
 universes u
 
 /-

library/Init/Data/Repr.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic
-import init.data.uint
-import init.data.nat.div
+import Init.Data.String.Basic
+import Init.Data.Uint
+import Init.Data.Nat.Div
 open Sum Subtype Nat
 
 universes u v

library/Init/Data/String/Basic.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.list.basic
-import init.data.char.basic
-import init.data.option.basic
+import Init.Data.List.Basic
+import Init.Data.Char.Basic
+import Init.Data.Option.Basic
 universes u
 
 structure String :=

library/Init/Data/String/Default.lean

@@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic
+import Init.Data.String.Basic

library/Init/Data/ToString.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.data.string.basic
-import init.data.uint
-import init.data.nat.div
-import init.data.repr
+import Init.Data.String.Basic
+import Init.Data.Uint
+import Init.Data.Nat.Div
+import Init.Data.Repr
 open Sum Subtype Nat
 
 universes u v

library/Init/Data/UInt.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.fin.basic
-import init.system.platform
+import Init.Data.Fin.Basic
+import Init.System.Platform
 
 open Nat
 

library/Init/Default.lean

@@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.core
-import init.control
-import init.data.basic
-import init.coe
-import init.wf
-import init.data
-import init.system
-import init.util
-import init.fix
+import Init.Core
+import Init.Control
+import Init.Data.Basic
+import Init.Coe
+import Init.Wf
+import Init.Data
+import Init.System
+import Init.Util
+import Init.Fix

library/Init/Fix.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.uint
+import Init.Data.Uint
 universe u
 
 def bfix1 {α β : Type u} (base : α → β) (rec : (α → β) → α → β) : Nat → α → β

library/Init/Lean/Attributes.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.scopes
-import init.lean.syntax
+import Init.Lean.Scopes
+import Init.Lean.Syntax
 
 namespace Lean
 

library/Init/Lean/Class.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.attributes
+import Init.Lean.Attributes
 
 namespace Lean
 

library/Init/Lean/Compiler/ClosedTermCache.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.environment
+import Init.Lean.Environment
 
 namespace Lean
 

library/Init/Lean/Compiler/ConstFolding.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.system.platform
-import init.lean.expr
-import init.lean.compiler.util
+import Init.System.Platform
+import Init.Lean.Expr
+import Init.Lean.Compiler.Util
 
 /- Constant folding for primitives that have special runtime support. -/
 

library/Init/Lean/Compiler/Default.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.inlineattrs
-import init.lean.compiler.specialize
-import init.lean.compiler.constfolding
-import init.lean.compiler.closedtermcache
-import init.lean.compiler.externattr
-import init.lean.compiler.implementedbyattr
-import init.lean.compiler.neverextractattr
-import init.lean.compiler.ir
+import Init.Lean.Compiler.Inlineattrs
+import Init.Lean.Compiler.Specialize
+import Init.Lean.Compiler.Constfolding
+import Init.Lean.Compiler.Closedtermcache
+import Init.Lean.Compiler.Externattr
+import Init.Lean.Compiler.Implementedbyattr
+import Init.Lean.Compiler.Neverextractattr
+import Init.Lean.Compiler.Ir

library/Init/Lean/Compiler/ExportAttr.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.attributes
+import Init.Lean.Attributes
 
 namespace Lean
 

library/Init/Lean/Compiler/ExternAttr.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.option.basic
-import init.lean.expr
-import init.lean.environment
-import init.lean.attributes
-import init.lean.projfns
+import Init.Data.Option.Basic
+import Init.Lean.Expr
+import Init.Lean.Environment
+import Init.Lean.Attributes
+import Init.Lean.Projfns
 
 namespace Lean
 

library/Init/Lean/Compiler/IR/Basic.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.array
-import init.lean.name
-import init.lean.kvmap
-import init.lean.format
-import init.lean.compiler.externattr
+import Init.Data.Array
+import Init.Lean.Name
+import Init.Lean.Kvmap
+import Init.Lean.Format
+import Init.Lean.Compiler.Externattr
 /-
 Implements (extended) λPure and λRc proposed in the article
 "Counting Immutable Beans", Sebastian Ullrich and Leonardo de Moura.

library/Init/Lean/Compiler/IR/Borrow.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.exportattr
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.normids
+import Init.Lean.Compiler.Exportattr
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Normids
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/Boxing.lean

@@ -4,16 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.data.assoclist
-import init.control.estate
-import init.control.reader
-import init.lean.runtime
-import init.lean.compiler.closedtermcache
-import init.lean.compiler.externattr
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.freevars
-import init.lean.compiler.ir.elimdead
+import Init.Data.Assoclist
+import Init.Control.Estate
+import Init.Control.Reader
+import Init.Lean.Runtime
+import Init.Lean.Compiler.Closedtermcache
+import Init.Lean.Compiler.Externattr
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Freevars
+import Init.Lean.Compiler.Ir.Elimdead
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/Checker.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.compilerm
+import Init.Lean.Compiler.Ir.Compilerm
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/CompilerM.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.reader
-import init.lean.environment
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.format
+import Init.Control.Reader
+import Init.Lean.Environment
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Format
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/Default.lean

@@ -4,21 +4,21 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.format
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.pushproj
-import init.lean.compiler.ir.elimdead
-import init.lean.compiler.ir.simpcase
-import init.lean.compiler.ir.resetreuse
-import init.lean.compiler.ir.normids
-import init.lean.compiler.ir.checker
-import init.lean.compiler.ir.borrow
-import init.lean.compiler.ir.boxing
-import init.lean.compiler.ir.rc
-import init.lean.compiler.ir.expandresetreuse
-import init.lean.compiler.ir.unboxresult
-import init.lean.compiler.ir.emitc
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Format
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Pushproj
+import Init.Lean.Compiler.Ir.Elimdead
+import Init.Lean.Compiler.Ir.Simpcase
+import Init.Lean.Compiler.Ir.Resetreuse
+import Init.Lean.Compiler.Ir.Normids
+import Init.Lean.Compiler.Ir.Checker
+import Init.Lean.Compiler.Ir.Borrow
+import Init.Lean.Compiler.Ir.Boxing
+import Init.Lean.Compiler.Ir.Rc
+import Init.Lean.Compiler.Ir.Expandresetreuse
+import Init.Lean.Compiler.Ir.Unboxresult
+import Init.Lean.Compiler.Ir.Emitc
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/ElimDead.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.freevars
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Freevars
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/EmitC.lean

@@ -4,16 +4,16 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.conditional
-import init.lean.runtime
-import init.lean.compiler.namemangling
-import init.lean.compiler.exportattr
-import init.lean.compiler.initattr
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.emitutil
-import init.lean.compiler.ir.normids
-import init.lean.compiler.ir.simpcase
-import init.lean.compiler.ir.boxing
+import Init.Control.Conditional
+import Init.Lean.Runtime
+import Init.Lean.Compiler.Namemangling
+import Init.Lean.Compiler.Exportattr
+import Init.Lean.Compiler.Initattr
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Emitutil
+import Init.Lean.Compiler.Ir.Normids
+import Init.Lean.Compiler.Ir.Simpcase
+import Init.Lean.Compiler.Ir.Boxing
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/EmitUtil.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.conditional
-import init.lean.compiler.initattr
-import init.lean.compiler.ir.compilerm
+import Init.Control.Conditional
+import Init.Lean.Compiler.Initattr
+import Init.Lean.Compiler.Ir.Compilerm
 
 /- Helper functions for backend code generators -/
 

library/Init/Lean/Compiler/IR/ExpandResetReuse.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.state
-import init.control.reader
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.normids
-import init.lean.compiler.ir.freevars
+import Init.Control.State
+import Init.Control.Reader
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Normids
+import Init.Lean.Compiler.Ir.Freevars
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/Format.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.format
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Format
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/FreeVars.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
+import Init.Lean.Compiler.Ir.Basic
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/LiveVars.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.freevars
-import init.control.reader
-import init.control.conditional
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Freevars
+import Init.Control.Reader
+import Init.Control.Conditional
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/NormIds.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.reader
-import init.control.conditional
-import init.lean.compiler.ir.basic
+import Init.Control.Reader
+import Init.Control.Conditional
+import Init.Lean.Compiler.Ir.Basic
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/PushProj.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.freevars
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Freevars
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/RC.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.runtime
-import init.lean.compiler.ir.compilerm
-import init.lean.compiler.ir.livevars
+import Init.Lean.Runtime
+import Init.Lean.Compiler.Ir.Compilerm
+import Init.Lean.Compiler.Ir.Livevars
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/ResetReuse.lean

@@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.state
-import init.control.reader
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.livevars
-import init.lean.compiler.ir.format
+import Init.Control.State
+import Init.Control.Reader
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Livevars
+import Init.Lean.Compiler.Ir.Format
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/SimpCase.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.compiler.ir.format
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Compiler.Ir.Format
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/UnboxResult.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.compiler.ir.basic
-import init.lean.format
+import Init.Lean.Compiler.Ir.Basic
+import Init.Lean.Format
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/IR/UnreachBranches.lean

@@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.control.reader
-import init.data.option
-import init.lean.compiler.ir.format
-import init.lean.compiler.ir.basic
+import Init.Control.Reader
+import Init.Data.Option
+import Init.Lean.Compiler.Ir.Format
+import Init.Lean.Compiler.Ir.Basic
 
 namespace Lean
 namespace IR

library/Init/Lean/Compiler/ImplementedByAttr.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.attributes
+import Init.Lean.Attributes
 
 namespace Lean
 namespace Compiler

library/Init/Lean/Compiler/InitAttr.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.environment
-import init.lean.attributes
+import Init.Lean.Environment
+import Init.Lean.Attributes
 
 namespace Lean
 

library/Init/Lean/Compiler/InlineAttrs.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.attributes
-import init.lean.compiler.util
+import Init.Lean.Attributes
+import Init.Lean.Compiler.Util
 
 namespace Lean
 namespace Compiler

library/Init/Lean/Compiler/NameMangling.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
 prelude
-import init.lean.name
+import Init.Lean.Name
 namespace Lean
 
 private def String.mangleAux : Nat → String.Iterator → String → String

library/Init/Lean/Compiler/NeverExtractAttr.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
-import init.lean.environment
-import init.lean.attributes
+import Init.Lean.Environment
+import Init.Lean.Attributes
 
 namespace Lean