max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: remove typeclass assumptions for Nodup.eraseP (#4790)

Browse source 
The `α` in the typeclass assumptions wasn't even the element type of the
list.
This commit is contained in:
Markus Himmel 2024-07-21 09:51:42 +02:00 • committed by GitHub
parent bdfaa00b1e
commit 08acf5a136
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Init/Data/List/Lemmas.lean
View file

@ -3082,7 +3082,7 @@ theorem eraseP_eq_iff {p} {l : List α} :
(replicate n a).eraseP p = replicate n a := by
rw [eraseP_of_forall_not (by simp_all)]
theorem Nodup.eraseP [BEq α] [LawfulBEq α] (p) : Nodup l → Nodup (l.eraseP p) :=
theorem Nodup.eraseP (p) : Nodup l → Nodup (l.eraseP p) :=
Nodup.sublist <| eraseP_sublist _
theorem eraseP_comm {l : List α} (h : ∀ a ∈ l, ¬ p a ∨ ¬ q a) :