imports

leanprover · Sep 4, 2024 · f07f751 · f07f751
1 parent 85a7c1c
commit f07f751
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/src/Init/Data/Bool.lean b/src/Init/Data/Bool.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: F. G. Dorais
 -/
 prelude
-import Init.BinderPredicates
+import Init.NotationExtra
 
 /-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne

diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean
@@ -8,9 +8,8 @@ import Init.Data.Bool
 import Init.Data.Option.Lemmas
 import Init.Data.List.BasicAux
 import Init.Data.List.Control
-import Init.PropLemmas
 import Init.Control.Lawful.Basic
-import Init.Hints
+import Init.BinderPredicates
 
 /-! # Theorems about `List` operations.