refactor(library/init): move algebra to its own folder
This commit is contained in:
parent
e237109434
commit
af6ee4ad9d
9 changed files with 6 additions and 7 deletions
|
|
@ -4,4 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.group init.ordered_group init.ring init.ordered_ring
|
||||
import init.algebra.group init.algebra.ordered_group init.algebra.ring init.algebra.ordered_ring init.algebra.norm_num
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Robert Lewis and Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.ring
|
||||
import init.algebra.ring
|
||||
|
||||
namespace norm_num
|
||||
universe variable u
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Jeremy Avigad, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.group
|
||||
import init.algebra.order init.algebra.group
|
||||
|
||||
/- Make sure instances defined in this file have lower priority than the ones
|
||||
defined for concrete structures -/
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Jeremy Avigad, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.ordered_group init.ring
|
||||
import init.algebra.ordered_group init.algebra.ring
|
||||
|
||||
/- Make sure instances defined in this file have lower priority than the ones
|
||||
defined for concrete structures -/
|
||||
|
|
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
|
|||
Authors: Jeremy Avigad, Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.group
|
||||
import init.algebra.group
|
||||
|
||||
/- Make sure instances defined in this file have lower priority than the ones
|
||||
defined for concrete structures -/
|
||||
|
|
@ -12,5 +12,5 @@ import init.monad init.option init.state init.fin init.list init.char init.strin
|
|||
import init.monad_combinators init.set
|
||||
import init.timeit init.trace init.unsigned init.ordering init.list_classes init.coe
|
||||
import init.wf init.nat_div init.meta init.instances init.breakpoint
|
||||
import init.sigma_lex init.id_locked init.order init.algebra
|
||||
import init.sigma_lex init.id_locked init.algebra
|
||||
import init.nat_lemmas init.char_lemmas init.string_lemmas
|
||||
|
|
|
|||
|
|
@ -5,7 +5,6 @@ Authors: Floris van Doorn, Leonardo de Moura
|
|||
-/
|
||||
prelude
|
||||
import init.relation init.num
|
||||
import init.order
|
||||
|
||||
notation `ℕ` := nat
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue