~/bend-docscommunity

src/list.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/list.bend as MList

1 import
import Base

Laws

law append_nil provedsource · line 23 · raw

@-A:Data -> @xs:List<&2, A> -> {xs == List.append(&2, A, xs, []) : List<&2, A>}

law append_assoc provedsource · line 36 · raw

@-A:Data -> @a:List<&2, A> -> @-b:List<&2, A> -> @-c:List<&2, A> -> {List.append(&2, A, a, List.append(&2, A, b, c)) == List.append(&2, A, List.append(&2, A, a, b), c) : List<&2, A>}

law reverse_go provedsource · line 53 · raw

@-A:Data -> @+xs:List<&2, A> -> @+acc:List<&2, A> -> {List.append(&2, A, List.reverse(&2, A, xs), acc) == List.reverse.go(&2, A, xs, acc) : List<&2, A>}

List.reverse is List.reverse.go(xs, Nil{}); this says what the accumulator does.

Types

type Step source · line 12 · raw

@-a:Quant -> @-A:Data -> @-S:Kind(a) -> Kind(a)

One step of reading a sequence: nothing left, or an element and the rest. The quantity a is the rest's: &2 for a list, &1 for a linear queue.

Definitions

def uncons source · line 16 · raw

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