def insert_by_sorted

bend-mathlib@0.8.1.0 · sort.bend:76

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

76# Inserting into a sorted list keeps it sorted, for a total comparator.
77def insert_by_sorted(~A: Data, ~le: A -> A -> Bool, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, +x: A, +xs: List<&2, A>, +h: MList.sorted_by(~A, ~le, xs)) -> MList.sorted_by(~A, ~le, MPerm.insert_by(~A, ~le, x, xs)):
78  match xs:
79    case Nil{}:
80      internal_sorted_single(~A, ~le, x)
81    case +y <> t:
82      internal_insert_step(~A, ~le, ~le_total, le(x, y), x, y, t, {==}, h)