@[inline]

def Array.insertionSort {α : Type u_1} (xs : Array α) (lt : α → α → Bool := by exact (· < ·)) : Array α

Sorts an array using insertion sort.

The optional parameter lt specifies an ordering predicate. It defaults to LT.lt, which must be decidable to be used for sorting.

Equations

• xs.insertionSort lt = Array.insertionSort.traverse✝ lt xs 0 xs.size