diff --git a/library/Init/Coe.lean b/library/Init/Coe.lean index c8ef699d64..8007eda38e 100644 --- a/library/Init/Coe.lean +++ b/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) := diff --git a/library/Init/Control/Alternative.lean b/library/Init/Control/Alternative.lean index 1e354f8d10..6b5754dfb8 100644 --- a/library/Init/Control/Alternative.lean +++ b/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) := diff --git a/library/Init/Control/Applicative.lean b/library/Init/Control/Applicative.lean index fc963e28b7..5bde41de2c 100644 --- a/library/Init/Control/Applicative.lean +++ b/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 diff --git a/library/Init/Control/Combinators.lean b/library/Init/Control/Combinators.lean index c713a42bca..349b482c46 100644 --- a/library/Init/Control/Combinators.lean +++ b/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₃ diff --git a/library/Init/Control/Conditional.lean b/library/Init/Control/Conditional.lean index d3816ea9d7..9e6b4d3269 100644 --- a/library/Init/Control/Conditional.lean +++ b/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) := diff --git a/library/Init/Control/Default.lean b/library/Init/Control/Default.lean index 1e5fa3d67c..c384a7061f 100644 --- a/library/Init/Control/Default.lean +++ b/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 diff --git a/library/Init/Control/Estate.lean b/library/Init/Control/Estate.lean index 96d6884160..3b91228286 100644 --- a/library/Init/Control/Estate.lean +++ b/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 diff --git a/library/Init/Control/Except.lean b/library/Init/Control/Except.lean index 49ad3cbc62..697586d99d 100644 --- a/library/Init/Control/Except.lean +++ b/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) diff --git a/library/Init/Control/Functor.lean b/library/Init/Control/Functor.lean index 26b869c80f..46235c3bcf 100644 --- a/library/Init/Control/Functor.lean +++ b/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 diff --git a/library/Init/Control/Id.lean b/library/Init/Control/Id.lean index 95d289a03d..7bbe9f963c 100644 --- a/library/Init/Control/Id.lean +++ b/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 diff --git a/library/Init/Control/Lift.lean b/library/Init/Control/Lift.lean index d7843026d4..7df63101b2 100644 --- a/library/Init/Control/Lift.lean +++ b/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 diff --git a/library/Init/Control/Monad.lean b/library/Init/Control/Monad.lean index fa9adc92d5..01a1930068 100644 --- a/library/Init/Control/Monad.lean +++ b/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 diff --git a/library/Init/Control/Monadfail.lean b/library/Init/Control/Monadfail.lean index 1a084e2dfa..877af50dff 100644 --- a/library/Init/Control/Monadfail.lean +++ b/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 diff --git a/library/Init/Control/Option.lean b/library/Init/Control/Option.lean index f448b85089..93a088210e 100644 --- a/library/Init/Control/Option.lean +++ b/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 diff --git a/library/Init/Control/Reader.lean b/library/Init/Control/Reader.lean index a0ab19c207..53f67ab9fc 100644 --- a/library/Init/Control/Reader.lean +++ b/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) -/ diff --git a/library/Init/Control/State.lean b/library/Init/Control/State.lean index 1d1252a790..b85cba65d6 100644 --- a/library/Init/Control/State.lean +++ b/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) := diff --git a/library/Init/Data/Array/Basic.lean b/library/Init/Data/Array/Basic.lean index 2f3f77bde9..a3e24ed4c2 100644 --- a/library/Init/Data/Array/Basic.lean +++ b/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 /- diff --git a/library/Init/Data/Array/BinSearch.lean b/library/Init/Data/Array/BinSearch.lean index 3a904d6810..495254cee3 100644 --- a/library/Init/Data/Array/BinSearch.lean +++ b/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 diff --git a/library/Init/Data/Array/Default.lean b/library/Init/Data/Array/Default.lean index 0097930324..e36c8fccbb 100644 --- a/library/Init/Data/Array/Default.lean +++ b/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 diff --git a/library/Init/Data/Array/QSort.lean b/library/Init/Data/Array/QSort.lean index 934e124d0f..dff4618dee 100644 --- a/library/Init/Data/Array/QSort.lean +++ b/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 diff --git a/library/Init/Data/AssocList.lean b/library/Init/Data/AssocList.lean index 8ec939f354..4565ce0322 100644 --- a/library/Init/Data/AssocList.lean +++ b/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 -/ diff --git a/library/Init/Data/Basic.lean b/library/Init/Data/Basic.lean index b561940104..5e6dddab6a 100644 --- a/library/Init/Data/Basic.lean +++ b/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 diff --git a/library/Init/Data/BinomialHeap/Basic.lean b/library/Init/Data/BinomialHeap/Basic.lean index 3fec89152f..e71db56649 100644 --- a/library/Init/Data/BinomialHeap/Basic.lean +++ b/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 diff --git a/library/Init/Data/BinomialHeap/Default.lean b/library/Init/Data/BinomialHeap/Default.lean index a1af238505..dc6afb0e1b 100644 --- a/library/Init/Data/BinomialHeap/Default.lean +++ b/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 diff --git a/library/Init/Data/ByteArray/Basic.lean b/library/Init/Data/ByteArray/Basic.lean index ca889f4a5c..4011283694 100644 --- a/library/Init/Data/ByteArray/Basic.lean +++ b/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 := diff --git a/library/Init/Data/ByteArray/Default.lean b/library/Init/Data/ByteArray/Default.lean index d8bf710493..dc8e903181 100644 --- a/library/Init/Data/ByteArray/Default.lean +++ b/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 diff --git a/library/Init/Data/Char/Basic.lean b/library/Init/Data/Char/Basic.lean index 65d8185cdf..35b517b915 100644 --- a/library/Init/Data/Char/Basic.lean +++ b/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) diff --git a/library/Init/Data/Char/Default.lean b/library/Init/Data/Char/Default.lean index a383af31bd..dc2257bbfe 100644 --- a/library/Init/Data/Char/Default.lean +++ b/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 diff --git a/library/Init/Data/DList.lean b/library/Init/Data/DList.lean index d790f6e8e7..227fc057c6 100644 --- a/library/Init/Data/DList.lean +++ b/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 diff --git a/library/Init/Data/Default.lean b/library/Init/Data/Default.lean index 996c30bade..d3c7913925 100644 --- a/library/Init/Data/Default.lean +++ b/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 diff --git a/library/Init/Data/Fin/Basic.lean b/library/Init/Data/Fin/Basic.lean index 61a2ccaf9b..e115b16e32 100644 --- a/library/Init/Data/Fin/Basic.lean +++ b/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) diff --git a/library/Init/Data/Fin/Default.lean b/library/Init/Data/Fin/Default.lean index d3e08907ec..4e571c0f4b 100644 --- a/library/Init/Data/Fin/Default.lean +++ b/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 diff --git a/library/Init/Data/HashMap/Basic.lean b/library/Init/Data/HashMap/Basic.lean index adeae65d6e..5c1ffff325 100644 --- a/library/Init/Data/HashMap/Basic.lean +++ b/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) := diff --git a/library/Init/Data/HashMap/Default.lean b/library/Init/Data/HashMap/Default.lean index 868f956616..5d36df2c8f 100644 --- a/library/Init/Data/HashMap/Default.lean +++ b/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 diff --git a/library/Init/Data/Hashable.lean b/library/Init/Data/Hashable.lean index 124930ee68..75174e2896 100644 --- a/library/Init/Data/Hashable.lean +++ b/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) := diff --git a/library/Init/Data/Int/Basic.lean b/library/Init/Data/Int/Basic.lean index deffe9e2ae..2f078c9770 100644 --- a/library/Init/Data/Int/Basic.lean +++ b/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 -/ diff --git a/library/Init/Data/Int/Default.lean b/library/Init/Data/Int/Default.lean index a6abbc610b..55959e95bd 100644 --- a/library/Init/Data/Int/Default.lean +++ b/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 diff --git a/library/Init/Data/List/Basic.lean b/library/Init/Data/List/Basic.lean index a6134d3d37..c973d74729 100644 --- a/library/Init/Data/List/Basic.lean +++ b/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 diff --git a/library/Init/Data/List/BasicAux.lean b/library/Init/Data/List/BasicAux.lean index a69fb484e6..6e3b2d521d 100644 --- a/library/Init/Data/List/BasicAux.lean +++ b/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 diff --git a/library/Init/Data/List/Default.lean b/library/Init/Data/List/Default.lean index 20ced555ab..bd64f45b6b 100644 --- a/library/Init/Data/List/Default.lean +++ b/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 diff --git a/library/Init/Data/List/Instances.lean b/library/Init/Data/List/Instances.lean index 1f882877e4..7a92dd1b9f 100644 --- a/library/Init/Data/List/Instances.lean +++ b/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 diff --git a/library/Init/Data/Nat/Basic.lean b/library/Init/Data/Nat/Basic.lean index 8c7594480d..3a6e5c3381 100644 --- a/library/Init/Data/Nat/Basic.lean +++ b/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 diff --git a/library/Init/Data/Nat/Bitwise.lean b/library/Init/Data/Nat/Bitwise.lean index 80d81369ff..52a89b7a89 100644 --- a/library/Init/Data/Nat/Bitwise.lean +++ b/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 diff --git a/library/Init/Data/Nat/Default.lean b/library/Init/Data/Nat/Default.lean index 321ba7db66..6e5092226b 100644 --- a/library/Init/Data/Nat/Default.lean +++ b/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 diff --git a/library/Init/Data/Nat/Div.lean b/library/Init/Data/Nat/Div.lean index 5b70d5eae0..d1132b74ae 100644 --- a/library/Init/Data/Nat/Div.lean +++ b/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 := diff --git a/library/Init/Data/Option/Basic.lean b/library/Init/Data/Option/Basic.lean index e364a0e1d4..64f6b9aad6 100644 --- a/library/Init/Data/Option/Basic.lean +++ b/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 diff --git a/library/Init/Data/Option/BasicAux.lean b/library/Init/Data/Option/BasicAux.lean index b2b1c832a7..2a74f19c6a 100644 --- a/library/Init/Data/Option/BasicAux.lean +++ b/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 diff --git a/library/Init/Data/Option/Default.lean b/library/Init/Data/Option/Default.lean index 2a6f37c309..c175932ca8 100644 --- a/library/Init/Data/Option/Default.lean +++ b/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 diff --git a/library/Init/Data/Option/Instances.lean b/library/Init/Data/Option/Instances.lean index 9bd25dca91..f18c711701 100644 --- a/library/Init/Data/Option/Instances.lean +++ b/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 diff --git a/library/Init/Data/PersistentArray/Basic.lean b/library/Init/Data/PersistentArray/Basic.lean index 7121559138..1363ab00c5 100644 --- a/library/Init/Data/PersistentArray/Basic.lean +++ b/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) diff --git a/library/Init/Data/PersistentArray/Default.lean b/library/Init/Data/PersistentArray/Default.lean index c6da178b65..d5316dad8f 100644 --- a/library/Init/Data/PersistentArray/Default.lean +++ b/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 diff --git a/library/Init/Data/PersistentHashMap/Basic.lean b/library/Init/Data/PersistentHashMap/Basic.lean index 50fbbc6453..a924f10185 100644 --- a/library/Init/Data/PersistentHashMap/Basic.lean +++ b/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 diff --git a/library/Init/Data/PersistentHashMap/Default.lean b/library/Init/Data/PersistentHashMap/Default.lean index 7bce68ee64..44ebcf32e7 100644 --- a/library/Init/Data/PersistentHashMap/Default.lean +++ b/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 diff --git a/library/Init/Data/Queue/Basic.lean b/library/Init/Data/Queue/Basic.lean index a6f4d2ffb2..3b5f1f92f8 100644 --- a/library/Init/Data/Queue/Basic.lean +++ b/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) := diff --git a/library/Init/Data/Queue/Default.lean b/library/Init/Data/Queue/Default.lean index 681e670e86..68a6627db9 100644 --- a/library/Init/Data/Queue/Default.lean +++ b/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 diff --git a/library/Init/Data/RBMap/Basic.lean b/library/Init/Data/RBMap/Basic.lean index e22fd30962..e2a87a9614 100644 --- a/library/Init/Data/RBMap/Basic.lean +++ b/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' diff --git a/library/Init/Data/RBMap/BasicAux.lean b/library/Init/Data/RBMap/BasicAux.lean index 5a0695653d..be064d690f 100644 --- a/library/Init/Data/RBMap/BasicAux.lean +++ b/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' diff --git a/library/Init/Data/RBMap/Default.lean b/library/Init/Data/RBMap/Default.lean index 0b9431cf8c..e5e6fc320f 100644 --- a/library/Init/Data/RBMap/Default.lean +++ b/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 diff --git a/library/Init/Data/RBTree/Basic.lean b/library/Init/Data/RBTree/Basic.lean index e0a4d657d5..083ace947b 100644 --- a/library/Init/Data/RBTree/Basic.lean +++ b/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 := diff --git a/library/Init/Data/RBTree/Default.lean b/library/Init/Data/RBTree/Default.lean index 3c9fd609c1..6d77c501c1 100644 --- a/library/Init/Data/RBTree/Default.lean +++ b/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 diff --git a/library/Init/Data/Random.lean b/library/Init/Data/Random.lean index 1fa050a6f2..9daf26616d 100644 --- a/library/Init/Data/Random.lean +++ b/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 /- diff --git a/library/Init/Data/Repr.lean b/library/Init/Data/Repr.lean index ab74890600..d4b303ccee 100644 --- a/library/Init/Data/Repr.lean +++ b/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 diff --git a/library/Init/Data/String/Basic.lean b/library/Init/Data/String/Basic.lean index d76143434d..f9160960a0 100644 --- a/library/Init/Data/String/Basic.lean +++ b/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 := diff --git a/library/Init/Data/String/Default.lean b/library/Init/Data/String/Default.lean index aa5a1e84e5..88da4da708 100644 --- a/library/Init/Data/String/Default.lean +++ b/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 diff --git a/library/Init/Data/ToString.lean b/library/Init/Data/ToString.lean index db73e50fae..12ec24241d 100644 --- a/library/Init/Data/ToString.lean +++ b/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 diff --git a/library/Init/Data/UInt.lean b/library/Init/Data/UInt.lean index 8d563a86c0..4199d6d16e 100644 --- a/library/Init/Data/UInt.lean +++ b/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 diff --git a/library/Init/Default.lean b/library/Init/Default.lean index b4268ef7b0..09b59f1bc5 100644 --- a/library/Init/Default.lean +++ b/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 diff --git a/library/Init/Fix.lean b/library/Init/Fix.lean index bb5bb5a6ee..85d234762d 100644 --- a/library/Init/Fix.lean +++ b/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 → α → β diff --git a/library/Init/Lean/Attributes.lean b/library/Init/Lean/Attributes.lean index e7a66fdc3b..cad6b9dbae 100644 --- a/library/Init/Lean/Attributes.lean +++ b/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 diff --git a/library/Init/Lean/Class.lean b/library/Init/Lean/Class.lean index 7f37c4d8a8..755ff41682 100644 --- a/library/Init/Lean/Class.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ClosedTermCache.lean b/library/Init/Lean/Compiler/ClosedTermCache.lean index d20a05a08b..9afc4d4333 100644 --- a/library/Init/Lean/Compiler/ClosedTermCache.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ConstFolding.lean b/library/Init/Lean/Compiler/ConstFolding.lean index e143f9e029..2dd70fb11a 100644 --- a/library/Init/Lean/Compiler/ConstFolding.lean +++ b/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. -/ diff --git a/library/Init/Lean/Compiler/Default.lean b/library/Init/Lean/Compiler/Default.lean index a50e0a3ab7..d1a39d07be 100644 --- a/library/Init/Lean/Compiler/Default.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ExportAttr.lean b/library/Init/Lean/Compiler/ExportAttr.lean index f4e9640999..b6f5e97e98 100644 --- a/library/Init/Lean/Compiler/ExportAttr.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ExternAttr.lean b/library/Init/Lean/Compiler/ExternAttr.lean index 70664b6100..0b8db9ba25 100644 --- a/library/Init/Lean/Compiler/ExternAttr.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/Basic.lean b/library/Init/Lean/Compiler/IR/Basic.lean index fdfb0ee65a..d2c7d2f1e3 100644 --- a/library/Init/Lean/Compiler/IR/Basic.lean +++ b/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. diff --git a/library/Init/Lean/Compiler/IR/Borrow.lean b/library/Init/Lean/Compiler/IR/Borrow.lean index c280972141..5e205ee524 100644 --- a/library/Init/Lean/Compiler/IR/Borrow.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/Boxing.lean b/library/Init/Lean/Compiler/IR/Boxing.lean index f9a03ea028..08d30de1ba 100644 --- a/library/Init/Lean/Compiler/IR/Boxing.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/Checker.lean b/library/Init/Lean/Compiler/IR/Checker.lean index 9287858a78..c400061f30 100644 --- a/library/Init/Lean/Compiler/IR/Checker.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/CompilerM.lean b/library/Init/Lean/Compiler/IR/CompilerM.lean index 67c245ab31..bf097af226 100644 --- a/library/Init/Lean/Compiler/IR/CompilerM.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/Default.lean b/library/Init/Lean/Compiler/IR/Default.lean index 7089abb482..8d80faf36d 100644 --- a/library/Init/Lean/Compiler/IR/Default.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/ElimDead.lean b/library/Init/Lean/Compiler/IR/ElimDead.lean index f4eff69df7..ecd659f482 100644 --- a/library/Init/Lean/Compiler/IR/ElimDead.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/EmitC.lean b/library/Init/Lean/Compiler/IR/EmitC.lean index 578a2eeeee..5cb22c8c3d 100644 --- a/library/Init/Lean/Compiler/IR/EmitC.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/EmitUtil.lean b/library/Init/Lean/Compiler/IR/EmitUtil.lean index 626b546c7c..5c9ced0a46 100644 --- a/library/Init/Lean/Compiler/IR/EmitUtil.lean +++ b/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 -/ diff --git a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean b/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean index b8b8660437..27e334fd77 100644 --- a/library/Init/Lean/Compiler/IR/ExpandResetReuse.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/Format.lean b/library/Init/Lean/Compiler/IR/Format.lean index f200f20ffe..c2ecdf5738 100644 --- a/library/Init/Lean/Compiler/IR/Format.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/FreeVars.lean b/library/Init/Lean/Compiler/IR/FreeVars.lean index 061ef998b4..6c0638e4d3 100644 --- a/library/Init/Lean/Compiler/IR/FreeVars.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/LiveVars.lean b/library/Init/Lean/Compiler/IR/LiveVars.lean index a5799d4c5b..c4e1bbb0e6 100644 --- a/library/Init/Lean/Compiler/IR/LiveVars.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/NormIds.lean b/library/Init/Lean/Compiler/IR/NormIds.lean index 76e6239b29..720f6b113c 100644 --- a/library/Init/Lean/Compiler/IR/NormIds.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/PushProj.lean b/library/Init/Lean/Compiler/IR/PushProj.lean index b18fcf3da4..1f43a4431f 100644 --- a/library/Init/Lean/Compiler/IR/PushProj.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/RC.lean b/library/Init/Lean/Compiler/IR/RC.lean index 828f2d2f77..db1bc0c53a 100644 --- a/library/Init/Lean/Compiler/IR/RC.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/ResetReuse.lean b/library/Init/Lean/Compiler/IR/ResetReuse.lean index db550c2245..0f617fa9b1 100644 --- a/library/Init/Lean/Compiler/IR/ResetReuse.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/SimpCase.lean b/library/Init/Lean/Compiler/IR/SimpCase.lean index ba63605b04..9ddd015b2e 100644 --- a/library/Init/Lean/Compiler/IR/SimpCase.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/UnboxResult.lean b/library/Init/Lean/Compiler/IR/UnboxResult.lean index 9fdc0bc7b8..bbad7706da 100644 --- a/library/Init/Lean/Compiler/IR/UnboxResult.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/IR/UnreachBranches.lean b/library/Init/Lean/Compiler/IR/UnreachBranches.lean index bf52c896f3..2779303f6d 100644 --- a/library/Init/Lean/Compiler/IR/UnreachBranches.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/ImplementedByAttr.lean b/library/Init/Lean/Compiler/ImplementedByAttr.lean index 1a589894bd..053fd673da 100644 --- a/library/Init/Lean/Compiler/ImplementedByAttr.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/InitAttr.lean b/library/Init/Lean/Compiler/InitAttr.lean index b495c85932..5412a4b5da 100644 --- a/library/Init/Lean/Compiler/InitAttr.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/InlineAttrs.lean b/library/Init/Lean/Compiler/InlineAttrs.lean index b739bcdb12..2699f063a3 100644 --- a/library/Init/Lean/Compiler/InlineAttrs.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/NameMangling.lean b/library/Init/Lean/Compiler/NameMangling.lean index 48710b3389..8258a345d6 100644 --- a/library/Init/Lean/Compiler/NameMangling.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/NeverExtractAttr.lean b/library/Init/Lean/Compiler/NeverExtractAttr.lean index 1a8da67fd8..c61f92dc0b 100644 --- a/library/Init/Lean/Compiler/NeverExtractAttr.lean +++ b/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 diff --git a/library/Init/Lean/Compiler/Specialize.lean b/library/Init/Lean/Compiler/Specialize.lean index 906a080076..4140366288 100644 --- a/library/Init/Lean/Compiler/Specialize.lean +++ b/library/Init/Lean/Compiler/Specialize.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 diff --git a/library/Init/Lean/Compiler/Util.lean b/library/Init/Lean/Compiler/Util.lean index 4a15a10ae3..1765405c4f 100644 --- a/library/Init/Lean/Compiler/Util.lean +++ b/library/Init/Lean/Compiler/Util.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 namespace Compiler diff --git a/library/Init/Lean/Declaration.lean b/library/Init/Lean/Declaration.lean index c4c48dfc51..2425fd561d 100644 --- a/library/Init/Lean/Declaration.lean +++ b/library/Init/Lean/Declaration.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.expr +import Init.Lean.Expr namespace Lean /-- diff --git a/library/Init/Lean/Default.lean b/library/Init/Lean/Default.lean index a3e1209657..8eae4fbf6f 100644 --- a/library/Init/Lean/Default.lean +++ b/library/Init/Lean/Default.lean @@ -4,18 +4,18 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.lean.path -import init.lean.compiler -import init.lean.environment -import init.lean.modifiers -import init.lean.projfns -import init.lean.runtime -import init.lean.attributes -import init.lean.parser -import init.lean.reducibilityattrs -import init.lean.elaborator -import init.lean.eqncompiler -import init.lean.class -import init.lean.localcontext -import init.lean.metavarcontext -import init.lean.typeclass +import Init.Lean.Path +import Init.Lean.Compiler +import Init.Lean.Environment +import Init.Lean.Modifiers +import Init.Lean.Projfns +import Init.Lean.Runtime +import Init.Lean.Attributes +import Init.Lean.Parser +import Init.Lean.Reducibilityattrs +import Init.Lean.Elaborator +import Init.Lean.Eqncompiler +import Init.Lean.Class +import Init.Lean.Localcontext +import Init.Lean.Metavarcontext +import Init.Lean.Typeclass diff --git a/library/Init/Lean/Elaborator/Alias.lean b/library/Init/Lean/Elaborator/Alias.lean index 7cf5741386..a6602ce3b4 100644 --- a/library/Init/Lean/Elaborator/Alias.lean +++ b/library/Init/Lean/Elaborator/Alias.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 diff --git a/library/Init/Lean/Elaborator/Basic.lean b/library/Init/Lean/Elaborator/Basic.lean index 703d9cfc1e..9a20c73c89 100644 --- a/library/Init/Lean/Elaborator/Basic.lean +++ b/library/Init/Lean/Elaborator/Basic.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.control.reader -import init.lean.metavarcontext -import init.lean.namegenerator -import init.lean.scopes -import init.lean.parser.module +import Init.Control.Reader +import Init.Lean.Metavarcontext +import Init.Lean.Namegenerator +import Init.Lean.Scopes +import Init.Lean.Parser.Module namespace Lean diff --git a/library/Init/Lean/Elaborator/Command.lean b/library/Init/Lean/Elaborator/Command.lean index e89c40d3b2..0d89584384 100644 --- a/library/Init/Lean/Elaborator/Command.lean +++ b/library/Init/Lean/Elaborator/Command.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.elaborator.alias -import init.lean.elaborator.basic -import init.lean.elaborator.resolvename -import init.lean.elaborator.term +import Init.Lean.Elaborator.Alias +import Init.Lean.Elaborator.Basic +import Init.Lean.Elaborator.Resolvename +import Init.Lean.Elaborator.Term namespace Lean namespace Elab diff --git a/library/Init/Lean/Elaborator/Default.lean b/library/Init/Lean/Elaborator/Default.lean index cd1917db4d..f1cd1f9629 100644 --- a/library/Init/Lean/Elaborator/Default.lean +++ b/library/Init/Lean/Elaborator/Default.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.elaborator.basic -import init.lean.elaborator.elabstrategyattrs -import init.lean.elaborator.command -import init.lean.elaborator.preterm -import init.lean.elaborator.term +import Init.Lean.Elaborator.Basic +import Init.Lean.Elaborator.Elabstrategyattrs +import Init.Lean.Elaborator.Command +import Init.Lean.Elaborator.Preterm +import Init.Lean.Elaborator.Term diff --git a/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean b/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean index 5f376fe0a6..35de1a41d3 100644 --- a/library/Init/Lean/Elaborator/ElabStrategyAttrs.lean +++ b/library/Init/Lean/Elaborator/ElabStrategyAttrs.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 /- diff --git a/library/Init/Lean/Elaborator/PreTerm.lean b/library/Init/Lean/Elaborator/PreTerm.lean index f6f052d688..9ebcd3a10c 100644 --- a/library/Init/Lean/Elaborator/PreTerm.lean +++ b/library/Init/Lean/Elaborator/PreTerm.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.lean.elaborator.basic +import Init.Lean.Elaborator.Basic namespace Lean diff --git a/library/Init/Lean/Elaborator/ResolveName.lean b/library/Init/Lean/Elaborator/ResolveName.lean index 4a8bbb075c..724458d84c 100644 --- a/library/Init/Lean/Elaborator/ResolveName.lean +++ b/library/Init/Lean/Elaborator/ResolveName.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.lean.modifiers -import init.lean.elaborator.alias -import init.lean.elaborator.basic +import Init.Lean.Modifiers +import Init.Lean.Elaborator.Alias +import Init.Lean.Elaborator.Basic namespace Lean namespace Elab diff --git a/library/Init/Lean/Elaborator/Term.lean b/library/Init/Lean/Elaborator/Term.lean index 4c42e9bc1a..8bf06d8d83 100644 --- a/library/Init/Lean/Elaborator/Term.lean +++ b/library/Init/Lean/Elaborator/Term.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.elaborator.alias -import init.lean.elaborator.basic -import init.lean.elaborator.preterm +import Init.Lean.Elaborator.Alias +import Init.Lean.Elaborator.Basic +import Init.Lean.Elaborator.Preterm namespace Lean namespace Elab diff --git a/library/Init/Lean/Environment.lean b/library/Init/Lean/Environment.lean index d6b08eed77..1f6332af4e 100644 --- a/library/Init/Lean/Environment.lean +++ b/library/Init/Lean/Environment.lean @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.system.io -import init.util -import init.data.bytearray -import init.lean.declaration -import init.lean.smap -import init.lean.path -import init.lean.localcontext +import Init.System.Io +import Init.Util +import Init.Data.Bytearray +import Init.Lean.Declaration +import Init.Lean.Smap +import Init.Lean.Path +import Init.Lean.Localcontext namespace Lean /- Opaque environment extension state. It is essentially the Lean version of a C `void *` diff --git a/library/Init/Lean/EqnCompiler/Default.lean b/library/Init/Lean/EqnCompiler/Default.lean index 82d44e9f46..682208da0b 100644 --- a/library/Init/Lean/EqnCompiler/Default.lean +++ b/library/Init/Lean/EqnCompiler/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.lean.eqncompiler.matchpattern +import Init.Lean.Eqncompiler.Matchpattern diff --git a/library/Init/Lean/EqnCompiler/MatchPattern.lean b/library/Init/Lean/EqnCompiler/MatchPattern.lean index 410afbc5b9..d1ce445bf6 100644 --- a/library/Init/Lean/EqnCompiler/MatchPattern.lean +++ b/library/Init/Lean/EqnCompiler/MatchPattern.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 EqnCompiler diff --git a/library/Init/Lean/Expr.lean b/library/Init/Lean/Expr.lean index 8f7788534c..dcc2358688 100644 --- a/library/Init/Lean/Expr.lean +++ b/library/Init/Lean/Expr.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.level -import init.lean.kvmap +import Init.Lean.Level +import Init.Lean.Kvmap namespace Lean diff --git a/library/Init/Lean/Format.lean b/library/Init/Lean/Format.lean index d6389220b0..8ccae14b1b 100644 --- a/library/Init/Lean/Format.lean +++ b/library/Init/Lean/Format.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import init.lean.options -import init.data.array +import Init.Lean.Options +import Init.Data.Array universes u v namespace Lean diff --git a/library/Init/Lean/KVMap.lean b/library/Init/Lean/KVMap.lean index 242f34124d..eef16745f5 100644 --- a/library/Init/Lean/KVMap.lean +++ b/library/Init/Lean/KVMap.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.name -import init.data.option.basic -import init.data.int +import Init.Lean.Name +import Init.Data.Option.Basic +import Init.Data.Int namespace Lean diff --git a/library/Init/Lean/Level.lean b/library/Init/Lean/Level.lean index cc85d8aeff..7bc36aa106 100644 --- a/library/Init/Lean/Level.lean +++ b/library/Init/Lean/Level.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.option.basic -import init.lean.name -import init.lean.format +import Init.Data.Option.Basic +import Init.Lean.Name +import Init.Lean.Format namespace Lean diff --git a/library/Init/Lean/LocalContext.lean b/library/Init/Lean/LocalContext.lean index 291d8a00b6..e5a05b75ec 100644 --- a/library/Init/Lean/LocalContext.lean +++ b/library/Init/Lean/LocalContext.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.persistentarray.basic -import init.data.persistenthashmap.basic -import init.lean.expr +import Init.Data.Persistentarray.Basic +import Init.Data.Persistenthashmap.Basic +import Init.Lean.Expr namespace Lean diff --git a/library/Init/Lean/Message.lean b/library/Init/Lean/Message.lean index ef9ae73394..ab38b8289f 100644 --- a/library/Init/Lean/Message.lean +++ b/library/Init/Lean/Message.lean @@ -6,8 +6,8 @@ Author: Sebastian Ullrich Message Type used by the Lean frontend -/ prelude -import init.data.tostring -import init.lean.position +import Init.Data.Tostring +import Init.Lean.Position namespace Lean def mkErrorStringWithPos (fileName : String) (line col : Nat) (msg : String) : String := diff --git a/library/Init/Lean/MetavarContext.lean b/library/Init/Lean/MetavarContext.lean index 6efbcffa92..49ef6b40da 100644 --- a/library/Init/Lean/MetavarContext.lean +++ b/library/Init/Lean/MetavarContext.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.localcontext +import Init.Lean.Localcontext namespace Lean diff --git a/library/Init/Lean/Modifiers.lean b/library/Init/Lean/Modifiers.lean index d4daa6bdbc..b9419c5694 100644 --- a/library/Init/Lean/Modifiers.lean +++ b/library/Init/Lean/Modifiers.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 diff --git a/library/Init/Lean/Name.lean b/library/Init/Lean/Name.lean index 9c8a1ac610..76964ed667 100644 --- a/library/Init/Lean/Name.lean +++ b/library/Init/Lean/Name.lean @@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import init.data.string.basic -import init.coe -import init.data.uint -import init.data.tostring -import init.data.hashable -import init.data.rbmap -import init.data.rbtree +import Init.Data.String.Basic +import Init.Coe +import Init.Data.Uint +import Init.Data.Tostring +import Init.Data.Hashable +import Init.Data.Rbmap +import Init.Data.Rbtree namespace Lean inductive Name diff --git a/library/Init/Lean/NameGenerator.lean b/library/Init/Lean/NameGenerator.lean index 30bdb3cbaa..a6c4d54c1c 100644 --- a/library/Init/Lean/NameGenerator.lean +++ b/library/Init/Lean/NameGenerator.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.name +import Init.Lean.Name namespace Lean diff --git a/library/Init/Lean/Options.lean b/library/Init/Lean/Options.lean index f4d4db7272..dfd407f14a 100644 --- a/library/Init/Lean/Options.lean +++ b/library/Init/Lean/Options.lean @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich and Leonardo de Moura -/ prelude -import init.lean.kvmap -import init.system.io -import init.control.combinators -import init.data.tostring +import Init.Lean.Kvmap +import Init.System.Io +import Init.Control.Combinators +import Init.Data.Tostring namespace Lean diff --git a/library/Init/Lean/Parser/Command.lean b/library/Init/Lean/Parser/Command.lean index e88f14b36f..2a9ffd12df 100644 --- a/library/Init/Lean/Parser/Command.lean +++ b/library/Init/Lean/Parser/Command.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.lean.parser.term +import Init.Lean.Parser.Term namespace Lean namespace Parser diff --git a/library/Init/Lean/Parser/Default.lean b/library/Init/Lean/Parser/Default.lean index 137a645d36..a1ef5626bc 100644 --- a/library/Init/Lean/Parser/Default.lean +++ b/library/Init/Lean/Parser/Default.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.lean.parser.parser -import init.lean.parser.level -import init.lean.parser.term -import init.lean.parser.command -import init.lean.parser.module +import Init.Lean.Parser.Parser +import Init.Lean.Parser.Level +import Init.Lean.Parser.Term +import Init.Lean.Parser.Command +import Init.Lean.Parser.Module diff --git a/library/Init/Lean/Parser/Identifier.lean b/library/Init/Lean/Parser/Identifier.lean index 701e430496..2365ae2818 100644 --- a/library/Init/Lean/Parser/Identifier.lean +++ b/library/Init/Lean/Parser/Identifier.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.char.basic +import Init.Data.Char.Basic namespace Lean diff --git a/library/Init/Lean/Parser/Level.lean b/library/Init/Lean/Parser/Level.lean index 5b43c30d9f..a573172f45 100644 --- a/library/Init/Lean/Parser/Level.lean +++ b/library/Init/Lean/Parser/Level.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.lean.parser.parser +import Init.Lean.Parser.Parser namespace Lean namespace Parser diff --git a/library/Init/Lean/Parser/Module.lean b/library/Init/Lean/Parser/Module.lean index 2c8f65e6d5..ce2d1bb2af 100644 --- a/library/Init/Lean/Parser/Module.lean +++ b/library/Init/Lean/Parser/Module.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.lean.message -import init.lean.parser.command +import Init.Lean.Message +import Init.Lean.Parser.Command namespace Lean namespace Parser diff --git a/library/Init/Lean/Parser/Parser.lean b/library/Init/Lean/Parser/Parser.lean index 98508390ff..95a03ef7e5 100644 --- a/library/Init/Lean/Parser/Parser.lean +++ b/library/Init/Lean/Parser/Parser.lean @@ -4,15 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.lean.position -import init.lean.syntax -import init.lean.toexpr -import init.lean.message -import init.lean.environment -import init.lean.attributes -import init.lean.parser.trie -import init.lean.parser.identifier -import init.lean.compiler.initattr +import Init.Lean.Position +import Init.Lean.Syntax +import Init.Lean.Toexpr +import Init.Lean.Message +import Init.Lean.Environment +import Init.Lean.Attributes +import Init.Lean.Parser.Trie +import Init.Lean.Parser.Identifier +import Init.Lean.Compiler.Initattr namespace Lean namespace Parser diff --git a/library/Init/Lean/Parser/Term.lean b/library/Init/Lean/Parser/Term.lean index feb9928b8f..9b14437d26 100644 --- a/library/Init/Lean/Parser/Term.lean +++ b/library/Init/Lean/Parser/Term.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.lean.parser.parser -import init.lean.parser.level +import Init.Lean.Parser.Parser +import Init.Lean.Parser.Level namespace Lean namespace Parser diff --git a/library/Init/Lean/Parser/Transform.lean b/library/Init/Lean/Parser/Transform.lean index 175c2f91d1..efbfbeee20 100644 --- a/library/Init/Lean/Parser/Transform.lean +++ b/library/Init/Lean/Parser/Transform.lean @@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura, Sebastian Ullrich -/ -import init.lean.parser.parser +import Init.Lean.Parser.Parser namespace Lean namespace Syntax diff --git a/library/Init/Lean/Parser/Trie.lean b/library/Init/Lean/Parser/Trie.lean index c016e7c1de..cd0975deda 100644 --- a/library/Init/Lean/Parser/Trie.lean +++ b/library/Init/Lean/Parser/Trie.lean @@ -6,8 +6,8 @@ Author: Sebastian Ullrich, Leonardo de Moura Trie for tokenizing the Lean language -/ prelude -import init.data.rbmap -import init.lean.format +import Init.Data.Rbmap +import Init.Lean.Format namespace Lean namespace Parser diff --git a/library/Init/Lean/Path.lean b/library/Init/Lean/Path.lean index 105828d771..37a692995c 100644 --- a/library/Init/Lean/Path.lean +++ b/library/Init/Lean/Path.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.system.io -import init.system.filepath -import init.data.array -import init.control.combinators -import init.lean.name +import Init.System.Io +import Init.System.Filepath +import Init.Data.Array +import Init.Control.Combinators +import Init.Lean.Name namespace Lean open System.FilePath (pathSeparator searchPathSeparator extSeparator) diff --git a/library/Init/Lean/Position.lean b/library/Init/Lean/Position.lean index 3597090545..c44e7ca75c 100644 --- a/library/Init/Lean/Position.lean +++ b/library/Init/Lean/Position.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.data.nat -import init.data.rbmap -import init.lean.format +import Init.Data.Nat +import Init.Data.Rbmap +import Init.Lean.Format namespace Lean diff --git a/library/Init/Lean/Projfns.lean b/library/Init/Lean/Projfns.lean index a524b32539..6e4dbbaa3f 100644 --- a/library/Init/Lean/Projfns.lean +++ b/library/Init/Lean/Projfns.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 diff --git a/library/Init/Lean/ReducibilityAttrs.lean b/library/Init/Lean/ReducibilityAttrs.lean index 688b73e065..ebb3324e5e 100644 --- a/library/Init/Lean/ReducibilityAttrs.lean +++ b/library/Init/Lean/ReducibilityAttrs.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 diff --git a/library/Init/Lean/Runtime.lean b/library/Init/Lean/Runtime.lean index cbdbe78905..5878c49f39 100644 --- a/library/Init/Lean/Runtime.lean +++ b/library/Init/Lean/Runtime.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.core +import Init.Core namespace Lean diff --git a/library/Init/Lean/SMap.lean b/library/Init/Lean/SMap.lean index 951b3b82d1..70b50de64c 100644 --- a/library/Init/Lean/SMap.lean +++ b/library/Init/Lean/SMap.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.hashmap -import init.data.persistenthashmap +import Init.Data.Hashmap +import Init.Data.Persistenthashmap universes u v w w' namespace Lean diff --git a/library/Init/Lean/Scopes.lean b/library/Init/Lean/Scopes.lean index 9719ca80c0..1a0defa1a6 100644 --- a/library/Init/Lean/Scopes.lean +++ b/library/Init/Lean/Scopes.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 diff --git a/library/Init/Lean/Syntax.lean b/library/Init/Lean/Syntax.lean index 2d0b7bfc91..d8e6439bb8 100644 --- a/library/Init/Lean/Syntax.lean +++ b/library/Init/Lean/Syntax.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich, Leonardo de Moura -/ prelude -import init.lean.name -import init.lean.format -import init.data.array +import Init.Lean.Name +import Init.Lean.Format +import Init.Data.Array namespace Lean structure SourceInfo := diff --git a/library/Init/Lean/ToExpr.lean b/library/Init/Lean/ToExpr.lean index 0a878ab123..9bea2784c0 100644 --- a/library/Init/Lean/ToExpr.lean +++ b/library/Init/Lean/ToExpr.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.expr +import Init.Lean.Expr universe u namespace Lean diff --git a/library/Init/Lean/Trace.lean b/library/Init/Lean/Trace.lean index 285ccad171..a9352b3835 100644 --- a/library/Init/Lean/Trace.lean +++ b/library/Init/Lean/Trace.lean @@ -4,11 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ prelude -import init.lean.format -import init.data.rbmap -import init.lean.position -import init.lean.name -import init.lean.options +import Init.Lean.Format +import Init.Data.Rbmap +import Init.Lean.Position +import Init.Lean.Name +import Init.Lean.Options universe u diff --git a/library/Init/Lean/TypeClass/Basic.lean b/library/Init/Lean/TypeClass/Basic.lean index 4485e82330..b9a2a1cafc 100644 --- a/library/Init/Lean/TypeClass/Basic.lean +++ b/library/Init/Lean/TypeClass/Basic.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam, Leonardo de Moura -/ prelude -import init.lean.environment -import init.lean.typeclass.synth +import Init.Lean.Environment +import Init.Lean.Typeclass.Synth namespace Lean namespace TypeClass diff --git a/library/Init/Lean/TypeClass/Context.lean b/library/Init/Lean/TypeClass/Context.lean index 498191b230..1b5a1a9507 100644 --- a/library/Init/Lean/TypeClass/Context.lean +++ b/library/Init/Lean/TypeClass/Context.lean @@ -8,9 +8,9 @@ Custom unifier for tabled typeclass resolution. Note: this file will be removed once the unifier is implemented in Lean. -/ prelude -import init.data.persistentarray -import init.lean.expr -import init.lean.metavarcontext +import Init.Data.Persistentarray +import Init.Lean.Expr +import Init.Lean.Metavarcontext namespace Lean namespace TypeClass diff --git a/library/Init/Lean/TypeClass/Default.lean b/library/Init/Lean/TypeClass/Default.lean index 2582ec284d..c39597b0bc 100644 --- a/library/Init/Lean/TypeClass/Default.lean +++ b/library/Init/Lean/TypeClass/Default.lean @@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Daniel Selsam, Leonardo de Moura -/ prelude -import init.lean.typeclass.basic +import Init.Lean.Typeclass.Basic diff --git a/library/Init/Lean/TypeClass/Synth.lean b/library/Init/Lean/TypeClass/Synth.lean index 7eefda1490..393351ddb6 100644 --- a/library/Init/Lean/TypeClass/Synth.lean +++ b/library/Init/Lean/TypeClass/Synth.lean @@ -8,13 +8,13 @@ Typeclass synthesis using tabled resolution. Note: this file will be need to be updated once the unifier is implemented in Lean. -/ prelude -import init.lean.expr -import init.lean.environment -import init.lean.class -import init.lean.metavarcontext -import init.lean.typeclass.context -import init.data.persistenthashmap -import init.data.queue +import Init.Lean.Expr +import Init.Lean.Environment +import Init.Lean.Class +import Init.Lean.Metavarcontext +import Init.Lean.Typeclass.Context +import Init.Data.Persistenthashmap +import Init.Data.Queue namespace Lean namespace TypeClass diff --git a/library/Init/Lean/Util.lean b/library/Init/Lean/Util.lean index 39c3281726..f94c6b9596 100644 --- a/library/Init/Lean/Util.lean +++ b/library/Init/Lean/Util.lean @@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -/ prelude -import init.system.io -import init.lean.position +import Init.System.Io +import Init.Lean.Position namespace Lean diff --git a/library/Init/System/Default.lean b/library/Init/System/Default.lean index cd7c00d908..c57d87b3ee 100644 --- a/library/Init/System/Default.lean +++ b/library/Init/System/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.system.io -import init.system.platform +import Init.System.Io +import Init.System.Platform diff --git a/library/Init/System/Filepath.lean b/library/Init/System/Filepath.lean index e1e12aeb69..6157f5f915 100644 --- a/library/Init/System/Filepath.lean +++ b/library/Init/System/Filepath.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.platform -import init.data.string.basic +import Init.System.Platform +import Init.Data.String.Basic namespace System namespace FilePath diff --git a/library/Init/System/IO.lean b/library/Init/System/IO.lean index c7f794ea17..d8ef175d39 100644 --- a/library/Init/System/IO.lean +++ b/library/Init/System/IO.lean @@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich -/ prelude -import init.control.estate -import init.data.string.basic -import init.system.filepath +import Init.Control.Estate +import Init.Data.String.Basic +import Init.System.Filepath /-- Like https://hackage.haskell.org/package/ghc-Prim-0.5.2.0/docs/GHC-Prim.html#t:RealWorld. Makes sure we never reorder `IO` operations. diff --git a/library/Init/System/Platform.lean b/library/Init/System/Platform.lean index 9fefa3c744..6f66784361 100644 --- a/library/Init/System/Platform.lean +++ b/library/Init/System/Platform.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.nat.basic +import Init.Data.Nat.Basic namespace System namespace Platform diff --git a/library/Init/Util.lean b/library/Init/Util.lean index b1ac59be1e..5b0bb21c93 100644 --- a/library/Init/Util.lean +++ b/library/Init/Util.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.string.basic -import init.data.tostring +import Init.Data.String.Basic +import Init.Data.Tostring universes u v /- debugging helper functions -/ diff --git a/library/Init/Wf.lean b/library/Init/Wf.lean index a2fef9d380..63d1317b3e 100644 --- a/library/Init/Wf.lean +++ b/library/Init/Wf.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.nat.basic +import Init.Data.Nat.Basic universes u v diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 4c85c97380..1e67ddf4ef 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura, Gabriel Ebner #include "runtime/sstream.h" #ifndef LEAN_DEFAULT_MODULE_FILE_NAME -#define LEAN_DEFAULT_MODULE_FILE_NAME "default" +#define LEAN_DEFAULT_MODULE_FILE_NAME "Default" #endif namespace lean {