Theorems · Definition

List.destutter

{α : Type u_1} → (R : α → α → Prop) → [DecidableRel R] → List α → List α

Greedily create a sublist of l such that, for every two adjacent elements a, b ∈ l, R a b holds. Mostly used with ≠; for example, destutter (≠) [1, 2, 2, 1, 1] = [1, 2, 1], destutter (≠) [1, 2, 3, 3] = [1, 2, 3], destutter (<) [1, 2, 5, 2, 3, 4, 9] = [1, 2, 5, 9].

Defined in

Mathlib.Data.List.Defs

Cited by

25 results in Mathlib

Foundations

Depth 8 from the axioms · uses no axioms

Assumes

DecidableRel