bendlib-kernel-list

Releases (1):
  1.0.0.0  0xb5c8145e53a6a127d611f45f602666ec  indexed  https://jend.leeeet.dev/files.txt?path=bendlib-kernel-list@1.0.0.0

Definitions (5):
  List.swap_head (https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=swap_head)
   # Swap the first two elements (no-op on lists shorter than two).
   def swap_head(-A: Data, xs: List<&2, A>) -> List<&2, A>:
  List.swap_at (https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=swap_at)
   # Swap positions i and i+1.
   def swap_at(-A: Data, +i: Nat, xs: List<&2, A>) -> List<&2, A>:
  List.apply (https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=apply)
   # Apply a list of adjacent swaps, left to right.
   def apply(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>) -> List<&2, A>:
  List.perm_steps (https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm_steps)
   # The derivation `perm_steps(A, steps, xs, ys)` holds when `apply(A, steps, xs)` is `ys`.
   def perm_steps(-A: Data, +steps: List<&2, Nat>, xs: List<&2, A>, ys: List<&2, A>) -> Data:
  List.perm (https://jend.leeeet.dev/definition.txt?path=bendlib-kernel-list@1.0.0.0/list.bend&name=perm)
   # Some swap derivation carries `xs` to `ys` (the existential `perm`).
   def perm(-A: Data, xs: List<&2, A>, ys: List<&2, A>) -> Data: