@[inline]

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

@[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 (Nat.succ fuel_2) = if h : i < Array.size a 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 < Array.size a) : Array α

Equations

• One or more equations did not get rendered due to their size.
• Array.insertionSort.swapLoop lt a 0 h = a