Insertion Sort as a Query Program

Insertion sort implemented as a FreeM (LEQuery α), making all comparison queries explicit.

@[reducible, inline]

abbrev Cslib.Query.orderedInsert {α : Type} (x : α) (xs : List α) : FreeM (LEQuery α) (List α)

Insert x into a sorted list using comparison queries.

Equations

• Cslib.Query.orderedInsert x xs = List.orderedInsertM Cslib.Query.LEQuery.ask x xs

@[reducible, inline]

abbrev Cslib.Query.insertionSort {α : Type} (xs : List α) : FreeM (LEQuery α) (List α)

Sort a list using insertion sort with comparison queries.

Equations

• Cslib.Query.insertionSort xs = List.insertionSortM Cslib.Query.LEQuery.ask xs