feat(library/init/data/int): import int by default
This commit is contained in:
parent
9119554835
commit
bcf15b0d39
3 changed files with 10 additions and 2 deletions
|
|
@ -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.list init.data.sum init.data.subtype
|
||||
import init.data.list init.data.sum init.data.subtype init.data.int
|
||||
|
|
|
|||
7
library/init/data/int/default.lean
Normal file
7
library/init/data/int/default.lean
Normal 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.int.basic init.data.int.order
|
||||
|
|
@ -5,7 +5,8 @@ Authors: Jeremy Avigad
|
|||
|
||||
The order relation on the integers.
|
||||
-/
|
||||
import .basic
|
||||
prelude
|
||||
import init.data.int.basic
|
||||
|
||||
namespace int
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue