~/bend-docscommunity

sort.bend checks

raw source on the hub · import bend-mathlib@0.3.0.0/sort.bend as Sort

bend-mathlib/sort.bend: insertion sort proved sorted over perm.bend's value defs (generic ~le).

4 imports
import Base
import ./nat.bend as MNat
import ./list.bend as MList
import ./perm.bend as MPerm

Definitions

def internal_le_flip_nat source · line 27 · raw

@x:Nat -> @y:Nat -> @e:{Nat.is_le(x, y) == False{} : Bool} -> {Nat.is_le(y, x) == True{} : Bool}

def isort_by_sorted_nat source · line 74 · raw

@+xs:List<&2, Nat> -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(Nat, Nat.is_le, 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.isort_by(Nat, Nat.is_le, xs))

Templates

template internal_sorted_single source · line 7 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, [x])

template internal_sorted_cons_cons_intro source · line 10 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @hxy:{le(x, y) == True{} : Bool} -> @hyt:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> t) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, x <> y <> t)

template internal_sorted_cons_cons_elim_le source · line 14 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, x <> y <> t) -> {le(x, y) == True{} : Bool}

template internal_sorted_cons_cons_elim_tail source · line 17 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, x <> y <> t) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> t)

template internal_sorted_tail source · line 20 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @+x:A -> @+xs:List<&2, A> -> @h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, x <> xs) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, xs)

template internal_cons_ins_step source · line 38 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @b:Bool -> @+y:A -> @+x:A -> @+z:A -> @+u:List<&2, A> -> @e:{le(x, z) == b : Bool} -> @hyx:{le(y, x) == True{} : Bool} -> @+h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> z <> u) -> @k:(@_:{le(z, x) == True{} : Bool} -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, z <> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.insert_by(A, le, x, u))) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> Bool.pick(List<&2, A>, b, x <> z <> u, z <> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.insert_by(A, le, x, u)))

template internal_sorted_cons_ins source · line 45 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @+t:List<&2, A> -> @+y:A -> @+x:A -> @hyx:{le(y, x) == True{} : Bool} -> @+h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> t) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.insert_by(A, le, x, t))

template internal_insert_step source · line 52 · raw

@-A:Data -> @-le:(@_:A -> @_:A -> Bool) -> @-le_total:(@x:A -> @y:A -> @_:{le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}) -> @b:Bool -> @+x:A -> @+y:A -> @+t:List<&2, A> -> @e:{le(x, y) == b : Bool} -> @+h:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, y <> t) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, Bool.pick(List<&2, A>, b, x <> y <> t, y <> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.insert_by(A, le, x, t)))

template insert_by_sorted source · line 59 · raw

@-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:0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, xs) -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.insert_by(A, le, x, xs))

template isort_by_sorted source · line 67 · raw

@-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> -> 0x74bdc843cd4bfb31bb6f7ba1eb38d231/list.sorted_by(A, le, 0x74bdc843cd4bfb31bb6f7ba1eb38d231/perm.isort_by(A, le, xs))

Insertion sort returns a sorted list.