Skip to content

Commit f710fe1

Browse files
committed
feat: splitOn_nil to use BEq instead of DecidableEq (#31679)
Generalizes this theorem with a quick change.
1 parent 885688d commit f710fe1

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

Mathlib/Data/List/SplitOn.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,7 @@ variable {α : Type*} (p : α → Bool) (xs : List α) (ls : List (List α))
1414
attribute [simp] splitAt_eq
1515

1616
@[simp]
17-
theorem splitOn_nil [DecidableEq α] (a : α) : [].splitOn a = [[]] :=
17+
theorem splitOn_nil [BEq α] (a : α) : [].splitOn a = [[]] :=
1818
rfl
1919

2020
@[simp]

0 commit comments

Comments
 (0)