diff --git a/library/init/data/list/basic_aux.lean b/library/init/data/list/basicaux.lean similarity index 100% rename from library/init/data/list/basic_aux.lean rename to library/init/data/list/basicaux.lean diff --git a/library/init/data/list/default.lean b/library/init/data/list/default.lean index d2f62e7190..366fc9a658 100644 --- a/library/init/data/list/default.lean +++ b/library/init/data/list/default.lean @@ -4,4 +4,4 @@ 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.basic_aux init.data.list.instances +import init.data.list.basic init.data.list.basicaux init.data.list.instances