~/bend-docscommunity

list.bend checks

raw source on the hub · import bendlib-kernel-list@1.0.0.0/list.bend as MList

bendlib-kernel-list: frozen step-list permutations over List, generic over -A: Data. Frozen set: swap_head, swap_at, apply, perm_steps, perm; the bytes are the type identity (F3).

1 import
import Base

Definitions

def swap_head source · line 6 · raw

@-A:Data -> @xs:List<&2, A> -> List<&2, A>

Swap the first two elements (no-op on lists shorter than two).

def swap_at source · line 18 · raw

@-A:Data -> @+i:Nat -> @xs:List<&2, A> -> List<&2, A>

Swap positions i and i+1.

def apply source · line 30 · raw

@-A:Data -> @+steps:List<&2, Nat> -> @xs:List<&2, A> -> List<&2, A>

Apply a list of adjacent swaps, left to right.

def perm_steps source · line 38 · raw

@-A:Data -> @+steps:List<&2, Nat> -> @xs:List<&2, A> -> @ys:List<&2, A> -> Data

The derivation perm_steps(A, steps, xs, ys) holds when apply(A, steps, xs) is ys.

def perm source · line 42 · raw

@-A:Data -> @xs:List<&2, A> -> @ys:List<&2, A> -> Data

Some swap derivation carries xs to ys (the existential perm).