mathlib documentation

data.dlist.basic

def dlist.join {α : Type u_1} :
list (dlist α)dlist α

Concatenates a list of difference lists to form a single difference list. Similar to list.join.

Equations
@[simp]
theorem dlist_singleton {α : Type u_1} {a : α} :

@[simp]
theorem dlist_lazy {α : Type u_1} {l : list α} :