diff --git a/library/init/data/default.lean b/library/init/data/default.lean index 2bb25112c3..5037c9d72a 100644 --- a/library/init/data/default.lean +++ b/library/init/data/default.lean @@ -5,3 +5,4 @@ Authors: Leonardo de Moura -/ prelude import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string +import init.data.instances diff --git a/library/init/instances.lean b/library/init/data/instances.lean similarity index 100% rename from library/init/instances.lean rename to library/init/data/instances.lean diff --git a/library/init/default.lean b/library/init/default.lean index 6d832cb9c0..660262dfeb 100644 --- a/library/init/default.lean +++ b/library/init/default.lean @@ -6,8 +6,7 @@ Authors: Leonardo de Moura prelude import init.core init.logic init.category init.data.basic import init.propext init.funext init.category.combinators init.function init.classical -import init.util init.coe init.wf init.meta init.instances -import init.algebra init.data +import init.util init.coe init.wf init.meta init.algebra init.data def debugger.attr : user_attribute := { name := `breakpoint,