src/tree.bend checks

raw source on the hub · import 0x5f97f469d15c04a181dae0e4e64e1d3d/src/tree.bend as Tree

2 imports

import Base
import ./class.bend as C

Laws

law reduce_foldr provedsource · line 52 · raw

@-A:Data -> @-m:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup<A> -> @t:Tree<A> -> @+acc:List<&2, A> -> @+z:A -> {0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup.op(A, m, reduce(A, m, t), List.foldr(&2, A, A, 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup.fn(A, m), acc, z)) == List.foldr(&2, A, A, 0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup.fn(A, m), to_list.go(A, t, acc), z) : A}

reduce agrees with foldr. With acc = Nil{}: {op(reduce(t), z) == foldr(to_list(t), z)}.

Types

type Tree source · line 17 · raw

@-A:Data -> Data

Tip
```
@-A:Data -> @x:A -> Tree<A>
```

Fork

@-A:Data -> @l:Tree<A> -> @r:Tree<A> -> Tree<A>

Definitions

def to_list.go source · line 30 · raw

@-A:Data -> @t:Tree<A> -> @acc:List<&2, A> -> List<&2, A>

the leaves, left to right, in front of acc

def to_list source · line 37 · raw

@-A:Data -> @t:Tree<A> -> List<&2, A>

Templates

template reduce source · line 21 · raw

@-A:Data -> @-m:0x5f97f469d15c04a181dae0e4e64e1d3d/src/class.Semigroup<A> -> @t:Tree<A> -> A

template build source · line 42 · raw

@-A:Data -> @-f:(@_:Nat -> A) -> @+d:Nat -> @+lo:Nat -> Tree<A>

a balanced tree with 2^d leaves f(lo), f(lo+1), ..., so both halves of each parallel call do the same amount of work