Theorems · Definition

List.dedup

{α : Type u_1} → [DecidableEq α] → List α → List α

dedup l removes duplicates from l (taking only the last occurrence). Defined as pwFilter (≠). See also eraseDups which keeps the first occurrence instead: `` dedup [2, 0, 1, 0, 2, 0] = [1, 2, 0] eraseDups [2, 0, 1, 0, 2, 0] = [2, 0, 1] ``

Defined in

Mathlib.Data.List.Defs

Cited by

47 results in Mathlib

Foundations

Depth 14 from the axioms · uses no axioms

Assumes

DecidableEq