def perm_steps

bendlib-kernel-list@1.0.0.0 · list.bend:37

import Base

37# The derivation `perm_steps(A, steps, xs, ys)` holds when `apply(A, steps, xs)` is `ys`.
38def perm_steps(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>, ys: List<&2, A>) -> Data:
39  {apply(A, steps, xs) == ys : List<&2, A>}