@[inline]

def Array.insertionSort {α : Type u_1} (a : Array α) (lt : α → α → Bool) : Array α

Equations

• a.insertionSort lt = Array.insertionSort.traverse lt a 0 a.size

@[specialize #[]]

def Array.insertionSort.traverse {α : Type u_1} (lt : α → α → Bool) (a : Array α) (i : Nat) (fuel : Nat) : Array α

Equations

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

@[specialize #[]]

def Array.insertionSort.swapLoop {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j : Nat) (h : j < a.size) : Array α

Equations

• Array.insertionSort.swapLoop lt a 0 h = a
• Array.insertionSort.swapLoop lt a j'.succ h = let_fun h' := ⋯; if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap ⟨j'.succ, h⟩ ⟨j', h'⟩) j' ⋯ else a