def merge_by_perm_nat

bend-mathlib@0.8.1.0 · perm.bend:157

import Base
import bendlib-kernel-list@1.0.0.0/list.bend as K

157# Merging two Nat lists permutes their concatenation.
158def merge_by_perm_nat(+xs: List<&2, Nat>, +ys: List<&2, Nat>) -> K.perm(Nat, List.append(&2, Nat, xs, ys), merge_by(~Nat, ~Nat.is_le, xs, ys)):
159  merge_by_perm(~Nat, ~Nat.is_le, xs, ys)