refactor(library/init): move instances.lean => init.data

This commit is contained in:
Leonardo de Moura 2016-12-02 16:25:27 -08:00
parent ed97ab486f
commit 46cb2dfd02
3 changed files with 2 additions and 2 deletions

View file

@ -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

View file

@ -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,