From db75c8e5cf227a89d8c3e6aa6167362defd5fef7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Oct 2019 08:56:31 -0700 Subject: [PATCH] chore(library/init/data/list): renamed `basic_aux` ==> `basicaux` @kha we are currently avoiding `_` in file names. I am not super happy with names such as `neverextractattr.lean`. I am open to a new name convention for .lean files in the stdlib. --- library/init/data/list/{basic_aux.lean => basicaux.lean} | 0 library/init/data/list/default.lean | 2 +- 2 files changed, 1 insertion(+), 1 deletion(-) rename library/init/data/list/{basic_aux.lean => basicaux.lean} (100%) 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