Sort.internal_merge_sorted_pick: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/sort.bend as Sort
Lines 154-159 of bend-mathlib@0.8.1.0/sort.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/sort.bend&start_line=154&end_line=159

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

def internal_merge_sorted_pick(~A: Data, ~le: A -> A -> Bool, ~le_trans: @x: A -> @y: A -> @z: A -> {le(x, y) == True{} : Bool} -> {le(y, z) == True{} : Bool} -> {le(x, z) == True{} : Bool}, ~le_total: @x: A -> @y: A -> {le(x, y) == False{} : Bool} -> {le(y, x) == True{} : Bool}, b: Bool, +x: A, +xt: List<&2, A>, +y: A, +yt: List<&2, A>, +e: {le(x, y) == b : Bool}, hx: MList.sorted_by(~A, ~le, x <> xt), hy: MList.sorted_by(~A, ~le, y <> yt), hm1: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, xt, y <> yt)), hm2: MList.sorted_by(~A, ~le, MPerm.merge_by(~A, ~le, x <> xt, yt))) -> MList.sorted_by(~A, ~le, Bool.pick(List<&2, A>, b, x <> MPerm.merge_by(~A, ~le, xt, y <> yt), y <> MPerm.merge_by(~A, ~le, x <> xt, yt))):
  match b:
    case True{}:
      internal_sorted_cons_of_least(~A, ~le, x, MPerm.merge_by(~A, ~le, xt, y <> yt), internal_least_merge(~A, ~le, x, xt, y <> yt, internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx), internal_least_intro(~A, ~le, x, y, yt, e, internal_least_trans(~A, ~le, ~le_trans, x, y, yt, e, internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)))), hm1)
    case False{}:
      internal_sorted_cons_of_least(~A, ~le, y, MPerm.merge_by(~A, ~le, x <> xt, yt), internal_least_merge(~A, ~le, y, x <> xt, yt, internal_least_intro(~A, ~le, y, x, xt, le_total(x, y, e), internal_least_trans(~A, ~le, ~le_trans, y, x, xt, le_total(x, y, e), internal_sorted_least_head(~A, ~le, ~le_trans, xt, x, hx))), internal_sorted_least_head(~A, ~le, ~le_trans, yt, y, hy)), hm2)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/list.bend&name=sorted_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=merge_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least_intro
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least_merge
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_least_trans
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_sorted_cons_of_least
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/sort.bend&name=internal_sorted_least_head