Documentation

Init.Data.Array.InsertionSort

@[inline]

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

Equations

Array.insertionSort a lt = Array.insertionSort.traverse lt a 0 (Array.size a)

@[specialize]

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

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) :