@[irreducible]

def Hex.List.merge {α : Type u_1} (le : α → α → Bool) (xs ys : List α) : List α

Kernel-reducible stable merge.

Equations

• Hex.List.merge le [] ys = ys
• Hex.List.merge le xs [] = xs
• Hex.List.merge le (x :: xs_2) (y :: ys_2) = if le x y = true then x :: Hex.List.merge le xs_2 (y :: ys_2) else y :: Hex.List.merge le (x :: xs_2) ys_2

theorem Hex.List.merge_eq {α : Type u_1} (le : α → α → Bool) (xs ys : List α) : merge le xs ys = xs.merge ys le

def Hex.List.sort {α : Type u_1} (xs : List α) (le : α → α → Bool) : List α

Stable merge sort with structural recursion and exposed implementation helpers. The fuel is the input length, which bounds the depth of its halving recursion.

Equations

• Hex.List.sort xs le = Hex.List.sort.go le xs.length xs

def Hex.List.sort.go {α : Type u_1} (le : α → α → Bool) : Nat → List α → List α

Equations

• One or more equations did not get rendered due to their size.
• Hex.List.sort.go le 0 a✝ = a✝
• Hex.List.sort.go le n.succ [] = []
• Hex.List.sort.go le n.succ [x_2] = [x_2]

@[simp]

theorem Hex.List.sort_eq {α : Type u_1} (le : α → α → Bool) (xs : List α) : sort xs le = xs.mergeSort le

The exposed sort agrees with core's stable merge sort for every comparator.

@[csimp]

theorem Hex.List.sort_eq_mergeSort : @sort = @List.mergeSort

Compiled code keeps core's efficient merge-sort implementation.