From 65368a0c853c8ec0e135844ad30664bbda39b271 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Nov 2017 16:12:57 -0800 Subject: [PATCH] refactor(library): rbtree lemmas do not need to be in init folder --- library/data/rbtree/default.lean | 6 ++++++ library/{init => }/data/rbtree/lemmas.lean | 5 +---- library/init/data/rbtree/basic.lean | 2 +- library/init/data/rbtree/default.lean | 4 ++-- 4 files changed, 10 insertions(+), 7 deletions(-) create mode 100644 library/data/rbtree/default.lean rename library/{init => }/data/rbtree/lemmas.lean (99%) diff --git a/library/data/rbtree/default.lean b/library/data/rbtree/default.lean new file mode 100644 index 0000000000..bcc7359af8 --- /dev/null +++ b/library/data/rbtree/default.lean @@ -0,0 +1,6 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +import data.rbtree.lemmas diff --git a/library/init/data/rbtree/lemmas.lean b/library/data/rbtree/lemmas.lean similarity index 99% rename from library/init/data/rbtree/lemmas.lean rename to library/data/rbtree/lemmas.lean index 69d5af986c..a67303dec7 100644 --- a/library/init/data/rbtree/lemmas.lean +++ b/library/data/rbtree/lemmas.lean @@ -1,11 +1,8 @@ /- Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Mario Carneiro +Authors: Leonardo de Moura -/ -prelude -import init.data.rbtree.basic init.meta init.data.nat - universes u v /- TODO(Leo): remove after we cleanup stdlib simp lemmas -/ diff --git a/library/init/data/rbtree/basic.lean b/library/init/data/rbtree/basic.lean index 457e430193..ca3616b183 100644 --- a/library/init/data/rbtree/basic.lean +++ b/library/init/data/rbtree/basic.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Mario Carneiro +Authors: Leonardo de Moura -/ prelude import init.data.ordering diff --git a/library/init/data/rbtree/default.lean b/library/init/data/rbtree/default.lean index c09428e0a8..28812c78c3 100644 --- a/library/init/data/rbtree/default.lean +++ b/library/init/data/rbtree/default.lean @@ -1,10 +1,10 @@ /- Copyright (c) 2017 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Mario Carneiro +Authors: Leonardo de Moura -/ prelude -import init.data.rbtree.basic init.data.rbtree.lemmas +import init.data.rbtree.basic meta def rbtree.default_lt : tactic unit := `[apply has_lt.lt]