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