def isort_by_perm_nat

bend-mathlib@0.8.1.0 · perm.bend:106

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

106# Insertion sort permutes a Nat list.
107def isort_by_perm_nat(+xs: List<&2, Nat>) -> K.perm(Nat, xs, isort_by(~Nat, ~Nat.is_le, xs)):
108  isort_by_perm(~Nat, ~Nat.is_le, xs)