Documentation

Init.Data.Array.InsertionSort

@[inline]

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

Equations

Array.insertionSort a lt = (fun traverse swapLoop => traverse a 0 (Array.size a)) (Array.insertionSort.traverse lt) (Array.insertionSort.swapLoop lt)

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

Equations

Array.insertionSort.swapLoop lt a 0 h = a
Array.insertionSort.swapLoop lt a (Nat.succ j') h = (fun h' => if lt (Array.get a { val := Nat.succ j', isLt := h }) (Array.get a { val := j', isLt := h' }) = true then Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' (_ : j' < Array.size (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' })) else a) (_ : j' < Array.size a)