chore(data/list/lex): make data.list.lex not depend on data.list.basic (

#9750) Another simplification in list related dependencies, if this commit breaks external code the fix is to add `import data.list.basic` to the broken file.
leanprover-community · Oct 16, 2021 · 998ab78 · 998ab78
1 parent 066a168
commit 998ab78
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/data/list/lex.lean b/src/data/list/lex.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.list.basic
+import order.rel_classes
 
 /-!
 # Lexicographic ordering of lists.