def merge_by

bend-mathlib@0.8.1.0 · perm.bend:130

import Base

130# Merges two lists, taking the head of xs first whenever le(x, y) holds.
131def merge_by(~A: Data, ~le: A -> A -> Bool, xs: List<&2, A>, ys: List<&2, A>) -> List<&2, A>:
132  match xs ys:
133    case Nil{} _:
134      ys
135    case +x <> +xt Nil{}:
136      x <> xt
137    case +x <> +xt +y <> +yt:
138      Bool.pick(List<&2, A>, le(x, y), x <> merge_by(~A, ~le, xt, y <> yt), y <> merge_by(~A, ~le, x <> xt, yt))