def isort_by_sorted

bend-mathlib@0.8.1.0 · sort.bend:84

import Base
import bend-mathlib@0.8.1.0/list.bend as MList
import bend-mathlib@0.8.1.0/perm.bend as MPerm

84# Insertion sort returns a sorted list.
85def isort_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +xs: List<&2, A>) -> MList.sorted_by(~A, ~le, MPerm.isort_by(~A, ~le, xs)):
86  match xs:
87    case Nil{}:
88      {==}
89    case +x <> t:
90      insert_by_sorted(~A, ~le, ~le_total, x, MPerm.isort_by(~A, ~le, t), isort_by_sorted(~A, ~le, ~le_total, t))