refactor(library/init): list classes => instances

This commit is contained in:
Leonardo de Moura 2016-12-02 16:29:15 -08:00
parent 46cb2dfd02
commit e4285bf684
4 changed files with 14 additions and 4 deletions

View file

@ -4,6 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import init.data.setoid init.data.quot init.data.bool.basic init.data.unit init.data.nat.basic init.data.prod init.data.sum.basic
import init.data.num.basic init.data.sigma.basic init.data.subtype init.data.fin.basic init.data.list.basic init.data.char.basic init.data.string.basic
import init.data.option.basic init.data.set init.data.unsigned init.data.ordering init.data.list.classes init.data.to_string
import init.data.setoid init.data.quot init.data.bool.basic init.data.unit
import init.data.nat.basic init.data.prod init.data.sum.basic
import init.data.num.basic init.data.sigma.basic init.data.subtype
import init.data.fin.basic init.data.list.basic init.data.char.basic
import init.data.string.basic init.data.option.basic init.data.set
import init.data.unsigned init.data.ordering init.data.to_string

View file

@ -5,4 +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
import init.data.list init.data.instances

View file

@ -0,0 +1,7 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
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