diff --git a/library/init/data/default.lean b/library/init/data/default.lean index 6fd0e7a959..edbab1e2c3 100644 --- a/library/init/data/default.lean +++ b/library/init/data/default.lean @@ -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 diff --git a/library/init/data/int/default.lean b/library/init/data/int/default.lean new file mode 100644 index 0000000000..fe5a3c761e --- /dev/null +++ b/library/init/data/int/default.lean @@ -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 diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean index eb8cf081c1..36faaf0fbb 100644 --- a/library/init/data/int/order.lean +++ b/library/init/data/int/order.lean @@ -5,7 +5,8 @@ Authors: Jeremy Avigad The order relation on the integers. -/ -import .basic +prelude +import init.data.int.basic namespace int