def isort_by_perm

bend-mathlib@0.8.1.0 · perm.bend:98

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

98# Insertion sort permutes its input.
99def isort_by_perm(~A: Data, ~le: A -> A -> Bool, +xs: List<&2, A>) -> K.perm(A, xs, isort_by(~A, ~le, xs)):
100  match xs:
101    case Nil{}:
102      perm_refl(A, Nil{})
103    case +x <> t:
104      perm_trans(A, x <> t, x <> isort_by(~A, ~le, t), isort_by(~A, ~le, x <> t), perm_cons(A, x, t, isort_by(~A, ~le, t), isort_by_perm(~A, ~le, t)), insert_by_perm(~A, ~le, x, isort_by(~A, ~le, t)))