@[inline]

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

Equations

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

@[specialize #[]]

def Array.insertionSort.traverse {α : Type u_1} (lt : α → α → Bool := by exact (· < ·)) (a : Array α) (i 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 := by exact (· < ·)) (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 = if lt a[j'.succ] a[j'] = true then Array.insertionSort.swapLoop lt (a.swap j'.succ j' h ⋯) j' ⋯ else a