chore: upstream Std.Data.List.Init.Lemmas (#3341)

leanprover · Feb 15, 2024 · fae5b2e · fae5b2e
1 parent 2bd1870
commit fae5b2e
Show file tree

Hide file tree

Showing 5 changed files with 633 additions and 9 deletions.
diff --git a/src/Init/Data/List.lean b/src/Init/Data/List.lean
@@ -7,3 +7,4 @@ prelude
 import Init.Data.List.Basic
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
+import Init.Data.List.Lemmas