Perm.msort_by_perm: def of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/perm.bend as Perm
Lines 233-239 of bend-mathlib@0.8.1.0/perm.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/perm.bend&start_line=233&end_line=239

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

# Merge sort permutes its input, for any fuel.
def msort_by_perm(~A: Data, ~le: A -> A -> Bool, fuel: Nat, +xs: List<&2, A>) -> K.perm(A, xs, msort_by(~A, ~le, fuel, xs)):
  match fuel:
    case 0n:
      perm_refl(A, xs)
    case 1n++f:
      perm_trans(A, xs, List.append(&2, A, evens(A, xs), odds(A, xs)), msort_by(~A, ~le, 1n+f, xs), split_perm(A, xs), perm_trans(A, List.append(&2, A, evens(A, xs), odds(A, xs)), List.append(&2, A, msort_by(~A, ~le, f, evens(A, xs)), msort_by(~A, ~le, f, odds(A, xs))), msort_by(~A, ~le, 1n+f, xs), perm_append(A, evens(A, xs), msort_by(~A, ~le, f, evens(A, xs)), odds(A, xs), msort_by(~A, ~le, f, odds(A, xs)), msort_by_perm(~A, ~le, f, evens(A, xs)), msort_by_perm(~A, ~le, f, odds(A, xs))), merge_by_perm(~A, ~le, msort_by(~A, ~le, f, evens(A, xs)), msort_by(~A, ~le, f, odds(A, xs)))))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=evens
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=merge_by_perm
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=msort_by
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=odds
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_append
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_refl
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=perm_trans
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/perm.bend&name=split_perm
  https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm