single version of List.removeAll?

Stream: Is there code for X?

[Malvin Gattinger]

I am wondering: List.erase is to List.diff like ??? is to List.removeAll?

import Batteries.Data.List.Basic

-- only removing first occurrence:
example : List.erase [1,2,2,1] 1 == [2,2,1] := by simp; decide -- single element to be removed
example : List.diff [1,2,2,1] [1] == [2,2,1] := by simp; decide -- list to be removed

-- removing all occurrences:
example : List.removeAll [1,2,2,1] [1] == [2,2] := by simp; decide -- list to be removed

-- Is this in Mathlib with a different name?
def List.remove [BEq α] (l : List α) (x : α) : List α := l.filter (fun y => x != y)

example : List.remove [1,2,2,1] 1 == [2,2] := by simp; decide

[Mario Carneiro]

l.filter (. != a)?

[Malvin Gattinger]

Okay, that is short enough :smile: I was just expecting a named function ;)

[SnO2WMaN]

Originally there was a List.remove, but for some reason it was removed in this PR. https://github.com/leanprover-community/mathlib4/pull/11846

I want to re-add this and some lemma about it since commonly used in our project, how about?

[Kim Morrison]

My preference is not to. Adding to the List API comes at huge expense if we actually want to reach a complete and mostly-confluent simp set. Keeping the API surface area smaller in the meantime is valuable.

[Malvin Gattinger]

Ah, thanks. So to make my definitions simp-able easily, should I use docs#List.removeAll with a singleton list as argument, or something like l.filter (. != a) from Mario above?

[Kim Morrison]

l.filter (. != a) is the preferred spelling, I think.