From e4285bf68470e678d88cdedf3dd154bba5e1a28c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 Dec 2016 16:29:15 -0800 Subject: [PATCH] refactor(library/init): list classes => instances --- library/init/data/basic.lean | 9 ++++++--- library/init/data/default.lean | 2 +- library/init/data/list/default.lean | 7 +++++++ library/init/data/list/{classes.lean => instances.lean} | 0 4 files changed, 14 insertions(+), 4 deletions(-) create mode 100644 library/init/data/list/default.lean rename library/init/data/list/{classes.lean => instances.lean} (100%) diff --git a/library/init/data/basic.lean b/library/init/data/basic.lean index 114ddf0dd2..351943d2fe 100644 --- a/library/init/data/basic.lean +++ b/library/init/data/basic.lean @@ -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 diff --git a/library/init/data/default.lean b/library/init/data/default.lean index 5037c9d72a..2b06cfb1f1 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.instances +import init.data.list init.data.instances diff --git a/library/init/data/list/default.lean b/library/init/data/list/default.lean new file mode 100644 index 0000000000..869f13423b --- /dev/null +++ b/library/init/data/list/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.list.basic init.data.list.instances diff --git a/library/init/data/list/classes.lean b/library/init/data/list/instances.lean similarity index 100% rename from library/init/data/list/classes.lean rename to library/init/data/list/instances.lean