Zulip Chat Archive
Stream: Is there code for X?
Topic: Pairwise erase
Marcus Rossel (Aug 28 2024 at 16:16):
Does this exist anywhere?
example [DecidableEq α] {l : List α} {p} (a : α) (h : l.Pairwise p) : (l.erase a).Pairwise p
Yaël Dillies (Aug 28 2024 at 16:21):
Kim Morrison (Aug 28 2024 at 22:59):
Added (Pairwise|Nodup).erase(|P|idx) in lean#5196.
Last updated: May 02 2025 at 03:31 UTC