From 2ea0baeb99f9eb9ffe0da16bf0dba8de93a94036 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Mar 2019 16:28:31 -0700 Subject: [PATCH] chore(library): use lowercase in imports --- library/init/IO.lean | 2 +- library/init/Lean/Parser/basic.lean | 6 +++--- library/init/Lean/Parser/combinators.lean | 4 ++-- library/init/Lean/Parser/command.lean | 2 +- library/init/Lean/Parser/declaration.lean | 2 +- library/init/Lean/Parser/identifier.lean | 2 +- library/init/Lean/Parser/level.lean | 2 +- library/init/Lean/Parser/module.lean | 2 +- library/init/Lean/Parser/notation.lean | 2 +- library/init/Lean/Parser/parsec.lean | 4 ++-- library/init/Lean/Parser/pratt.lean | 2 +- library/init/Lean/Parser/rec.lean | 2 +- library/init/Lean/Parser/stringLiteral.lean | 2 +- library/init/Lean/Parser/syntax.lean | 2 +- library/init/Lean/Parser/term.lean | 4 ++-- library/init/Lean/Parser/token.lean | 2 +- library/init/Lean/Parser/trie.lean | 4 ++-- library/init/Lean/compiler/constFolding.lean | 4 ++-- library/init/Lean/compiler/default.lean | 2 +- library/init/Lean/compiler/ir.lean | 2 +- library/init/Lean/compiler/util.lean | 2 +- library/init/Lean/declaration.lean | 2 +- library/init/Lean/default.lean | 6 +++--- library/init/Lean/disjoint_set.lean | 2 +- library/init/Lean/elaborator.lean | 8 ++++---- library/init/Lean/expander.lean | 4 ++-- library/init/Lean/expr.lean | 2 +- library/init/Lean/extern.lean | 2 +- library/init/Lean/format.lean | 2 +- library/init/Lean/frontend.lean | 2 +- library/init/Lean/kvmap.lean | 2 +- library/init/Lean/level.lean | 2 +- library/init/Lean/message.lean | 2 +- library/init/Lean/name.lean | 4 ++-- library/init/Lean/name_mangling.lean | 2 +- library/init/Lean/options.lean | 2 +- library/init/Lean/position.lean | 2 +- library/init/Lean/trace.lean | 2 +- library/init/Lean/util.lean | 2 +- library/init/coe.lean | 2 +- library/init/control/Alternative.lean | 2 +- library/init/control/Applicative.lean | 2 +- library/init/control/EState.lean | 2 +- library/init/control/Except.lean | 4 ++-- library/init/control/Functor.lean | 2 +- library/init/control/Monad.lean | 2 +- library/init/control/MonadFail.lean | 2 +- library/init/control/Option.lean | 2 +- library/init/control/Reader.lean | 2 +- library/init/control/State.lean | 4 ++-- library/init/control/combinators.lean | 2 +- library/init/control/default.lean | 8 ++++---- library/init/control/lift.lean | 4 ++-- library/init/data/array/basic.lean | 4 ++-- library/init/data/array/default.lean | 2 +- library/init/data/basic.lean | 8 ++++---- library/init/data/char/default.lean | 2 +- library/init/data/default.lean | 8 ++++---- library/init/data/dlist.lean | 2 +- library/init/data/fin/basic.lean | 2 +- library/init/data/fin/default.lean | 2 +- library/init/data/hashable.lean | 2 +- library/init/data/hashmap/basic.lean | 4 ++-- library/init/data/int/basic.lean | 2 +- library/init/data/int/default.lean | 2 +- library/init/data/list/basic.lean | 2 +- library/init/data/list/default.lean | 2 +- library/init/data/list/instances.lean | 4 ++-- library/init/data/nat/bitwise.lean | 2 +- library/init/data/nat/default.lean | 2 +- library/init/data/nat/div.lean | 2 +- library/init/data/option/basic.lean | 2 +- library/init/data/option/instances.lean | 2 +- library/init/data/rbmap/basic.lean | 2 +- library/init/data/rbmap/default.lean | 2 +- library/init/data/rbtree/basic.lean | 2 +- library/init/data/rbtree/default.lean | 2 +- library/init/data/repr.lean | 2 +- library/init/data/string/basic.lean | 6 +++--- library/init/data/string/default.lean | 2 +- library/init/data/toString.lean | 2 +- library/init/data/uint.lean | 2 +- library/init/default.lean | 4 ++-- library/init/util.lean | 2 +- library/init/wf.lean | 2 +- 85 files changed, 117 insertions(+), 117 deletions(-) diff --git a/library/init/IO.lean b/library/init/IO.lean index 83e2322b81..f604ff550e 100644 --- a/library/init/IO.lean +++ b/library/init/IO.lean @@ -4,7 +4,7 @@ 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 init.data.String.basic init.fix +import init.control.estate init.data.string.basic init.fix /-- 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/Lean/Parser/basic.lean b/library/init/Lean/Parser/basic.lean index e404d38dd3..fa5c4c9203 100644 --- a/library/init/Lean/Parser/basic.lean +++ b/library/init/Lean/Parser/basic.lean @@ -6,9 +6,9 @@ Author: Sebastian Ullrich Parser for the Lean language -/ prelude -import init.Lean.Parser.Parsec init.Lean.Parser.Syntax init.Lean.Parser.rec -import init.Lean.Parser.Trie -import init.Lean.Parser.identifier init.data.Rbmap init.Lean.Message +import init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.rec +import init.lean.parser.trie +import init.lean.parser.identifier init.data.rbmap init.lean.message namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/combinators.lean b/library/init/Lean/Parser/combinators.lean index 5562e8b9db..6d85222799 100644 --- a/library/init/Lean/Parser/combinators.lean +++ b/library/init/Lean/Parser/combinators.lean @@ -6,8 +6,8 @@ Author: Sebastian Ullrich Syntax-tree creating Parser Combinators -/ prelude -import init.Lean.Parser.basic -import init.data.List.instances +import init.lean.parser.basic +import init.data.list.instances namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/command.lean b/library/init/Lean/Parser/command.lean index d46f6390d3..de47cc00da 100644 --- a/library/init/Lean/Parser/command.lean +++ b/library/init/Lean/Parser/command.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Command parsers -/ prelude -import init.Lean.Parser.Declaration +import init.lean.parser.declaration namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/declaration.lean b/library/init/Lean/Parser/declaration.lean index 6cdd2b34a5..40c6679a9d 100644 --- a/library/init/Lean/Parser/declaration.lean +++ b/library/init/Lean/Parser/declaration.lean @@ -7,7 +7,7 @@ Parsers for commands that declare things -/ prelude -import init.Lean.Parser.Term +import init.lean.parser.term namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/identifier.lean b/library/init/Lean/Parser/identifier.lean index bcfdf92b00..a6c23cd3d0 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 init.Lean.Parser.Parsec +import init.data.char.basic init.lean.parser.parsec namespace Lean diff --git a/library/init/Lean/Parser/level.lean b/library/init/Lean/Parser/level.lean index 8d014686c2..94b54ea1ef 100644 --- a/library/init/Lean/Parser/level.lean +++ b/library/init/Lean/Parser/level.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Level-Level parsers -/ prelude -import init.Lean.Parser.pratt +import init.lean.parser.pratt namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/module.lean b/library/init/Lean/Parser/module.lean index 625b911407..e8ffe08504 100644 --- a/library/init/Lean/Parser/module.lean +++ b/library/init/Lean/Parser/module.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Module-Level parsers -/ prelude -import init.Lean.Parser.command +import init.lean.parser.command namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/notation.lean b/library/init/Lean/Parser/notation.lean index 226cb2002d..e1fe8af62b 100644 --- a/library/init/Lean/Parser/notation.lean +++ b/library/init/Lean/Parser/notation.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Notation parsers -/ prelude -import init.Lean.Parser.token +import init.lean.parser.token namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/parsec.lean b/library/init/Lean/Parser/parsec.lean index f16f857e3b..5f0ade61da 100644 --- a/library/init/Lean/Parser/parsec.lean +++ b/library/init/Lean/Parser/parsec.lean @@ -8,8 +8,8 @@ paper: https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Parsec-paper-letter.pdf -/ prelude -import init.data.toString init.data.String.basic init.data.List.basic init.control.Except -import init.data.repr init.Lean.Name init.data.Dlist init.control.MonadFail init.control.Combinators +import init.data.tostring init.data.string.basic init.data.list.basic init.control.except +import init.data.repr init.lean.name init.data.dlist init.control.monadfail init.control.combinators namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/pratt.lean b/library/init/Lean/Parser/pratt.lean index dde7db190e..90aca834c7 100644 --- a/library/init/Lean/Parser/pratt.lean +++ b/library/init/Lean/Parser/pratt.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich A Combinator for building Pratt parsers -/ prelude -import init.Lean.Parser.token +import init.lean.parser.token namespace Lean.Parser open MonadParsec Combinators diff --git a/library/init/Lean/Parser/rec.lean b/library/init/Lean/Parser/rec.lean index 969e95c5fc..39fc1dfe5a 100644 --- a/library/init/Lean/Parser/rec.lean +++ b/library/init/Lean/Parser/rec.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Recursion monad transformer -/ prelude -import init.Lean.Parser.Parsec init.fix +import init.lean.parser.parsec init.fix namespace Lean.Parser diff --git a/library/init/Lean/Parser/stringLiteral.lean b/library/init/Lean/Parser/stringLiteral.lean index 9a2291ab21..0440387bf3 100644 --- a/library/init/Lean/Parser/stringLiteral.lean +++ b/library/init/Lean/Parser/stringLiteral.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.Parser.Parsec +import init.lean.parser.parsec namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/syntax.lean b/library/init/Lean/Parser/syntax.lean index 0fd9464fe7..4f25d58f5f 100644 --- a/library/init/Lean/Parser/syntax.lean +++ b/library/init/Lean/Parser/syntax.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -/ prelude -import init.Lean.Name init.Lean.Parser.Parsec +import init.lean.name init.lean.parser.parsec namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/term.lean b/library/init/Lean/Parser/term.lean index a899ee5885..56d1b85889 100644 --- a/library/init/Lean/Parser/term.lean +++ b/library/init/Lean/Parser/term.lean @@ -6,8 +6,8 @@ Author: Sebastian Ullrich Term-Level parsers -/ prelude -import init.Lean.Parser.Level init.Lean.Parser.notation -import init.Lean.Expr +import init.lean.parser.level init.lean.parser.notation +import init.lean.expr namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/token.lean b/library/init/Lean/Parser/token.lean index 6813db3a9a..aaf5089566 100644 --- a/library/init/Lean/Parser/token.lean +++ b/library/init/Lean/Parser/token.lean @@ -13,7 +13,7 @@ the input String, we still use a "tokenizer" Parser in the Lean Parser in some c -/ prelude -import init.Lean.Parser.Combinators init.Lean.Parser.stringLiteral +import init.lean.parser.combinators init.lean.parser.stringliteral namespace Lean namespace Parser diff --git a/library/init/Lean/Parser/trie.lean b/library/init/Lean/Parser/trie.lean index e884581758..9578ae51be 100644 --- a/library/init/Lean/Parser/trie.lean +++ b/library/init/Lean/Parser/trie.lean @@ -6,8 +6,8 @@ Author: Sebastian Ullrich 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/compiler/constFolding.lean b/library/init/Lean/compiler/constFolding.lean index 01ce264b01..6ecb91c11d 100644 --- a/library/init/Lean/compiler/constFolding.lean +++ b/library/init/Lean/compiler/constFolding.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.Expr init.platform -import init.Lean.Compiler.util +import init.lean.expr init.platform +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 f5a28d1075..d30910f3a6 100644 --- a/library/init/Lean/compiler/default.lean +++ b/library/init/Lean/compiler/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.Compiler.constFolding +import init.lean.compiler.constfolding diff --git a/library/init/Lean/compiler/ir.lean b/library/init/Lean/compiler/ir.lean index 27b2ae2a60..e9ca6a7809 100644 --- a/library/init/Lean/compiler/ir.lean +++ b/library/init/Lean/compiler/ir.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 -/ -import init.Lean.Name init.Lean.Kvmap +import init.lean.name init.lean.kvmap prelude /- diff --git a/library/init/Lean/compiler/util.lean b/library/init/Lean/compiler/util.lean index 9f1e5056b2..cc65dee153 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.Expr +import init.lean.expr namespace Lean namespace Compiler diff --git a/library/init/Lean/declaration.lean b/library/init/Lean/declaration.lean index 61e172f4c8..8a55af5960 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 3443dd0ee3..d4994c0035 100644 --- a/library/init/Lean/default.lean +++ b/library/init/Lean/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.Lean.Compiler -import init.Lean.frontend -import init.Lean.extern +import init.lean.compiler +import init.lean.frontend +import init.lean.extern diff --git a/library/init/Lean/disjoint_set.lean b/library/init/Lean/disjoint_set.lean index 1e0d5ef125..682aead5b5 100644 --- a/library/init/Lean/disjoint_set.lean +++ b/library/init/Lean/disjoint_set.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.Hashmap.basic +import init.data.hashmap.basic /- Disjoint set datastructure using union-find algorithm. We use hashmaps to implement. Thus, we should be disjoint sets diff --git a/library/init/Lean/elaborator.lean b/library/init/Lean/elaborator.lean index 28f15d9cc7..d258ca5236 100644 --- a/library/init/Lean/elaborator.lean +++ b/library/init/Lean/elaborator.lean @@ -6,10 +6,10 @@ Author: Sebastian Ullrich Elaborator for the Lean language: takes commands and produces side effects -/ prelude -import init.Lean.Parser.Module -import init.Lean.Expander -import init.Lean.Expr -import init.Lean.Options +import init.lean.parser.module +import init.lean.expander +import init.lean.expr +import init.lean.options namespace Lean -- TODO(Sebastian): should probably be meta together with the whole Elaborator diff --git a/library/init/Lean/expander.lean b/library/init/Lean/expander.lean index 50294b6eea..73b1ce3080 100644 --- a/library/init/Lean/expander.lean +++ b/library/init/Lean/expander.lean @@ -9,8 +9,8 @@ TODO(Sebastian): document/link to documentation of algorithm -/ prelude -import init.Lean.Parser.Module -import init.Lean.Expr +import init.lean.parser.module +import init.lean.expr namespace Lean namespace Expander diff --git a/library/init/Lean/expr.lean b/library/init/Lean/expr.lean index 723b84d837..632ccaa473 100644 --- a/library/init/Lean/expr.lean +++ b/library/init/Lean/expr.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.Level init.Lean.Kvmap +import init.lean.level init.lean.kvmap namespace Lean diff --git a/library/init/Lean/extern.lean b/library/init/Lean/extern.lean index a09a4f900c..3ae5520ca4 100644 --- a/library/init/Lean/extern.lean +++ b/library/init/Lean/extern.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 init.data.Option.basic +import init.lean.expr init.data.option.basic namespace Lean diff --git a/library/init/Lean/format.lean b/library/init/Lean/format.lean index df6e9ad858..ae55745649 100644 --- a/library/init/Lean/format.lean +++ b/library/init/Lean/format.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.Except init.control.Reader init.control.State +import init.control.except init.control.reader init.control.state universes u v namespace Lean diff --git a/library/init/Lean/frontend.lean b/library/init/Lean/frontend.lean index 8fe2fc5350..22d6ec2966 100644 --- a/library/init/Lean/frontend.lean +++ b/library/init/Lean/frontend.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -/ -import init.Lean.Parser.Module init.Lean.Expander init.Lean.Elaborator init.Lean.util init.Io +import init.lean.parser.module init.lean.expander init.lean.elaborator init.lean.util init.io namespace Lean open Lean.Parser diff --git a/library/init/Lean/kvmap.lean b/library/init/Lean/kvmap.lean index 65954e771f..a01e143dbf 100644 --- a/library/init/Lean/kvmap.lean +++ b/library/init/Lean/kvmap.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 init.data.Option.basic +import init.lean.name init.data.option.basic namespace Lean diff --git a/library/init/Lean/level.lean b/library/init/Lean/level.lean index 78b6885f73..61cd478ba2 100644 --- a/library/init/Lean/level.lean +++ b/library/init/Lean/level.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 init.data.Option.basic +import init.lean.name init.data.option.basic namespace Lean diff --git a/library/init/Lean/message.lean b/library/init/Lean/message.lean index a564e9db26..c9766ea118 100644 --- a/library/init/Lean/message.lean +++ b/library/init/Lean/message.lean @@ -6,7 +6,7 @@ Author: Sebastian Ullrich Message Type used by the Lean frontend -/ prelude -import init.data.toString init.Lean.Position +import init.data.tostring init.lean.position namespace Lean inductive MessageSeverity diff --git a/library/init/Lean/name.lean b/library/init/Lean/name.lean index 5184f32c0e..198638b414 100644 --- a/library/init/Lean/name.lean +++ b/library/init/Lean/name.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.String.basic init.coe init.data.uint init.data.toString -import init.Lean.Format init.data.Hashable init.data.Rbmap init.data.Rbtree +import init.data.string.basic init.coe init.data.uint init.data.tostring +import init.lean.format init.data.hashable init.data.rbmap init.data.rbtree namespace Lean inductive Name diff --git a/library/init/Lean/name_mangling.lean b/library/init/Lean/name_mangling.lean index fda4d02cab..b2e4ef7206 100644 --- a/library/init/Lean/name_mangling.lean +++ b/library/init/Lean/name_mangling.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 init.Lean.Parser.stringLiteral +import init.lean.name init.lean.parser.stringliteral namespace Lean open Lean.Parser open Lean.Parser.MonadParsec diff --git a/library/init/Lean/options.lean b/library/init/Lean/options.lean index 85a21f7b28..46c63fef7d 100644 --- a/library/init/Lean/options.lean +++ b/library/init/Lean/options.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ prelude -import init.Lean.Kvmap +import init.lean.kvmap universe u namespace Lean diff --git a/library/init/Lean/position.lean b/library/init/Lean/position.lean index 7753d06060..167cfd5636 100644 --- a/library/init/Lean/position.lean +++ b/library/init/Lean/position.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.data.Nat init.data.Rbmap init.Lean.Format +import init.data.nat init.data.rbmap init.lean.format namespace Lean diff --git a/library/init/Lean/trace.lean b/library/init/Lean/trace.lean index 7e755457a1..49af1fed10 100644 --- a/library/init/Lean/trace.lean +++ b/library/init/Lean/trace.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Sebastian Ullrich -/ prelude -import init.Lean.Format init.data.Rbmap init.Lean.Position init.Lean.Name init.Lean.Options +import init.lean.format init.data.rbmap init.lean.position init.lean.name init.lean.options universe u diff --git a/library/init/Lean/util.lean b/library/init/Lean/util.lean index 6d6be4bf2e..5e6be0587b 100644 --- a/library/init/Lean/util.lean +++ b/library/init/Lean/util.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Sebastian Ullrich -/ prelude -import init.Lean.Position init.IO +import init.lean.position init.io namespace Lean diff --git a/library/init/coe.lean b/library/init/coe.lean index a7c1cafef6..863dd3f704 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 659304d609..c12ab92e03 100644 --- a/library/init/control/Alternative.lean +++ b/library/init/control/Alternative.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura -/ prelude -import init.core init.control.Applicative +import init.core init.control.applicative universes u v class HasOrelse (f : Type u → Type v) : Type (max (u+1) v) := diff --git a/library/init/control/Applicative.lean b/library/init/control/Applicative.lean index 690b46d882..3ca18e9f1b 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/EState.lean b/library/init/control/EState.lean index c44b677288..070ebc3c18 100644 --- a/library/init/control/EState.lean +++ b/library/init/control/EState.lean @@ -8,7 +8,7 @@ of memory allocations using the approach described in the paper "Counting immutable beans" by Sebastian and Leo -/ prelude -import init.control.State init.control.Except +import init.control.state init.control.except universes u v namespace Estate diff --git a/library/init/control/Except.lean b/library/init/control/Except.lean index 3f80b4f325..df13d5f4eb 100644 --- a/library/init/control/Except.lean +++ b/library/init/control/Except.lean @@ -6,8 +6,8 @@ Authors: Jared Roesch, Sebastian Ullrich The Except monad transformer. -/ prelude -import init.control.Alternative init.control.lift init.data.toString -import init.control.MonadFail +import init.control.alternative init.control.lift 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 88f274ce21..226ee6a0ff 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 init.Function +import init.core init.function open Function universes u v diff --git a/library/init/control/Monad.lean b/library/init/control/Monad.lean index 8a9792165a..b93041f6e0 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 open Function diff --git a/library/init/control/MonadFail.lean b/library/init/control/MonadFail.lean index b86c4ab296..356efffc3f 100644 --- a/library/init/control/MonadFail.lean +++ b/library/init/control/MonadFail.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.control.lift init.data.String.basic +import init.control.lift init.data.string.basic universes u v diff --git a/library/init/control/Option.lean b/library/init/control/Option.lean index 864a3ff2b8..89b8e86658 100644 --- a/library/init/control/Option.lean +++ b/library/init/control/Option.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.Alternative init.control.lift init.control.Except +import init.control.alternative init.control.lift init.control.except universes u v diff --git a/library/init/control/Reader.lean b/library/init/control/Reader.lean index f86fa3bc1f..2f214d85d9 100644 --- a/library/init/control/Reader.lean +++ b/library/init/control/Reader.lean @@ -7,7 +7,7 @@ The Reader monad transformer for passing immutable State. -/ prelude -import init.control.lift init.control.id init.control.Alternative init.control.Except +import init.control.lift init.control.id init.control.alternative 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 d7b3ab0a02..8019d0bb4d 100644 --- a/library/init/control/State.lean +++ b/library/init/control/State.lean @@ -6,8 +6,8 @@ Authors: Leonardo de Moura, Sebastian Ullrich The State monad transformer. -/ prelude -import init.control.Alternative init.control.lift -import init.control.id init.control.Except +import init.control.alternative init.control.lift +import init.control.id 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/control/combinators.lean b/library/init/control/combinators.lean index d6746fae1c..3c8e6cf00b 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura Monad Combinators, as in Haskell's Control.Monad. -/ prelude -import init.control.Monad init.control.Alternative init.data.List.basic init.coe +import init.control.monad init.control.alternative init.data.list.basic init.coe universes u v w @[specialize] diff --git a/library/init/control/default.lean b/library/init/control/default.lean index 7e13cf259d..fc6b0c2504 100644 --- a/library/init/control/default.lean +++ b/library/init/control/default.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.control.Applicative init.control.Functor init.control.Alternative -import init.control.Monad init.control.lift -import init.control.State init.control.id init.control.Except init.control.Reader -import init.control.Option init.control.Combinators +import init.control.applicative init.control.functor init.control.alternative +import init.control.monad init.control.lift +import init.control.state init.control.id init.control.except init.control.reader +import init.control.option init.control.combinators diff --git a/library/init/control/lift.lean b/library/init/control/lift.lean index d3a6512395..2d55f96aa6 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.Function init.coe -import init.control.Monad +import init.function init.coe +import init.control.monad universes u v w diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index e949f69321..1cfbbbe459 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/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.Nat.basic init.data.Fin.basic init.data.uint init.data.repr init.Function -import init.data.toString +import init.data.nat.basic init.data.fin.basic init.data.uint init.data.repr init.function +import init.data.tostring universes u v w /- diff --git a/library/init/data/array/default.lean b/library/init/data/array/default.lean index 0ee6a42816..0760a52cf6 100644 --- a/library/init/data/array/default.lean +++ b/library/init/data/array/default.lean @@ -4,4 +4,4 @@ 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.basic diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean index 29b0ad7978..cd9e8d9974 100644 --- a/library/init/data/basic.lean +++ b/library/init/data/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.Nat.basic init.data.Fin.basic init.data.List.basic init.data.Char.basic -import init.data.String.basic init.data.Option.basic -import init.data.uint init.data.Ordering.basic init.data.repr -import init.data.toString +import init.data.nat.basic init.data.fin.basic init.data.list.basic init.data.char.basic +import init.data.string.basic init.data.option.basic +import init.data.uint init.data.ordering.basic init.data.repr +import init.data.tostring diff --git a/library/init/data/char/default.lean b/library/init/data/char/default.lean index f1b6c21877..a383af31bd 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/default.lean b/library/init/data/default.lean index 49b749ed39..92735eb72f 100644 --- a/library/init/data/default.lean +++ b/library/init/data/default.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.basic init.data.Nat init.data.Char init.data.String -import init.data.List init.data.Int init.data.Array -import init.data.Fin init.data.uint init.data.Ordering -import init.data.Rbtree init.data.Rbmap init.data.Option.basic init.data.Option.instances +import init.data.basic init.data.nat init.data.char init.data.string +import init.data.list init.data.int init.data.array +import init.data.fin init.data.uint init.data.ordering +import init.data.rbtree init.data.rbmap init.data.option.basic init.data.option.instances diff --git a/library/init/data/dlist.lean b/library/init/data/dlist.lean index 9a9cbd3266..cc3c72dd7e 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 init.Function +import init.data.list.basic init.function universes u /-- A difference List is a Function that, given a List, returns the original diff --git a/library/init/data/fin/basic.lean b/library/init/data/fin/basic.lean index 61bf84afcd..9008c043e8 100644 --- a/library/init/data/fin/basic.lean +++ b/library/init/data/fin/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.Nat.div init.data.Nat.bitwise +import init.data.nat.div 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 92f55df0c0..d3e08907ec 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/hashable.lean b/library/init/data/hashable.lean index b3a846f576..415e683ffb 100644 --- a/library/init/data/hashable.lean +++ b/library/init/data/hashable.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 init.data.String +import init.data.uint init.data.string universes u class Hashable (α : Type u) := diff --git a/library/init/data/hashmap/basic.lean b/library/init/data/hashmap/basic.lean index c877484c50..52851a36c1 100644 --- a/library/init/data/hashmap/basic.lean +++ b/library/init/data/hashmap/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.Array.basic init.data.List.basic -import init.data.Option.basic init.data.Hashable +import init.data.array.basic init.data.list.basic +import init.data.option.basic init.data.hashable universes u v w def bucketArray (α : Type u) (β : α → Type v) := diff --git a/library/init/data/int/basic.lean b/library/init/data/int/basic.lean index d45c7bab38..0b5c72a497 100644 --- a/library/init/data/int/basic.lean +++ b/library/init/data/int/basic.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Leonardo de Moura The integers, with addition, multiplication, and subtraction. -/ prelude -import init.data.Nat.basic init.data.List init.coe init.data.repr init.data.toString +import init.data.nat.basic init.data.list init.coe init.data.repr 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 e0d4d7fc67..a6abbc610b 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 39c10b6d93..f5c4cfafd2 100644 --- a/library/init/data/list/basic.lean +++ b/library/init/data/list/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.core init.data.Nat.basic +import init.core init.data.nat.basic open Decidable List universes u v w diff --git a/library/init/data/list/default.lean b/library/init/data/list/default.lean index 295378f606..869f13423b 100644 --- a/library/init/data/list/default.lean +++ b/library/init/data/list/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.List.basic init.data.List.instances +import init.data.list.basic init.data.list.instances diff --git a/library/init/data/list/instances.lean b/library/init/data/list/instances.lean index a6364c78da..9f107ebf0c 100644 --- a/library/init/data/list/instances.lean +++ b/library/init/data/list/instances.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.control.Alternative init.control.Monad +import init.data.list.basic +import init.control.alternative init.control.monad open List universes u v diff --git a/library/init/data/nat/bitwise.lean b/library/init/data/nat/bitwise.lean index d2751afb7e..705243a6ab 100644 --- a/library/init/data/nat/bitwise.lean +++ b/library/init/data/nat/bitwise.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 init.data.Nat.div init.coe +import init.data.nat.basic init.data.nat.div init.coe namespace Nat def bitwise (f : Bool → Bool → Bool) : Nat → Nat → Nat | n m := diff --git a/library/init/data/nat/default.lean b/library/init/data/nat/default.lean index d4eea2946b..3efeb2636d 100644 --- a/library/init/data/nat/default.lean +++ b/library/init/data/nat/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.Nat.basic init.data.Nat.div init.data.Nat.bitwise +import init.data.nat.basic init.data.nat.div init.data.nat.bitwise diff --git a/library/init/data/nat/div.lean b/library/init/data/nat/div.lean index 2ba004578a..fc34cdeae1 100644 --- a/library/init/data/nat/div.lean +++ b/library/init/data/nat/div.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura -/ prelude -import init.wf init.data.Nat.basic +import init.wf 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 3c8382b3e6..3f2c350c50 100644 --- a/library/init/data/option/basic.lean +++ b/library/init/data/option/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.core init.control.Monad init.control.Alternative init.coe +import init.core init.control.monad init.control.alternative init.coe open Decidable universes u v diff --git a/library/init/data/option/instances.lean b/library/init/data/option/instances.lean index 6ae60b7914..6f56f3e03f 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/rbmap/basic.lean b/library/init/data/rbmap/basic.lean index 44eca881b5..15a5e2bba6 100644 --- a/library/init/data/rbmap/basic.lean +++ b/library/init/data/rbmap/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.Ordering.basic init.coe init.data.Option.basic +import init.data.ordering.basic init.coe init.data.option.basic universes u v w w' diff --git a/library/init/data/rbmap/default.lean b/library/init/data/rbmap/default.lean index 2912d82d8e..4d5a38b69a 100644 --- a/library/init/data/rbmap/default.lean +++ b/library/init/data/rbmap/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 init.data.Rbmap.basic +import init.data.rbtree init.data.rbmap.basic diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 42dd587b2f..9aa4916530 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 : α → α → Prop) : Type u := diff --git a/library/init/data/rbtree/default.lean b/library/init/data/rbtree/default.lean index 83b22e514a..3c9fd609c1 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/repr.lean b/library/init/data/repr.lean index 3ca4ff3a7b..5edcbb034a 100644 --- a/library/init/data/repr.lean +++ b/library/init/data/repr.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.String.basic init.data.uint init.data.Nat.div +import init.data.string.basic init.data.uint 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 ea883b80e6..004ba4f22b 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 /- In the VM, strings are implemented using a dynamic Array and UTF-8 encoding. TODO: mark as opaque -/ diff --git a/library/init/data/string/default.lean b/library/init/data/string/default.lean index 4055e9bcaa..aa5a1e84e5 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 406c48f2b7..6982c4d281 100644 --- a/library/init/data/toString.lean +++ b/library/init/data/toString.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.String.basic init.data.uint init.data.Nat.div init.data.repr +import init.data.string.basic init.data.uint init.data.nat.div 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 4729303338..f0a608b8aa 100644 --- a/library/init/data/uint.lean +++ b/library/init/data/uint.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.Fin.basic init.platform +import init.data.fin.basic init.platform open Nat diff --git a/library/init/default.lean b/library/init/default.lean index ac83d1cd6e..1515438f2e 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -5,5 +5,5 @@ Authors: Leonardo de Moura -/ prelude import init.core init.control init.data.basic -import init.Function init.coe init.wf -import init.data init.Io init.util init.fix +import init.function init.coe init.wf +import init.data init.io init.util init.fix diff --git a/library/init/util.lean b/library/init/util.lean index 394ce6b239..a24365590f 100644 --- a/library/init/util.lean +++ b/library/init/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.data.String.basic +import init.data.string.basic universes u /- debugging helper functions -/ diff --git a/library/init/wf.lean b/library/init/wf.lean index 72c45a4753..7627f12ce5 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