@[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

@[specialize #[]]

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

Equations

• Array.insertionSort.traverse lt xs i 0 = xs
• Array.insertionSort.traverse lt xs i fuel_2.succ = if h : i < xs.size then Array.insertionSort.traverse lt (Array.insertionSort.swapLoop lt xs i h) (i + 1) fuel_2 else xs

@[specialize #[]]

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

Equations

• Array.insertionSort.swapLoop lt xs 0 h = xs
• Array.insertionSort.swapLoop lt xs j'.succ h = if lt xs[j'.succ] xs[j'] = true then Array.insertionSort.swapLoop lt (xs.swap j'.succ j' h ⋯) j' ⋯ else xs