Data.Cotree

Definitions

record Cotree : Type -> Type

  A potentially infinite rose tree

Totality: total
Visibility: public export
Constructor: 

MkCotree : a -> Inf (Coforest a) -> Cotree a

Projections:

.forest : Cotree a -> Inf (Coforest a)

.value : Cotree a -> a

Hints:

Applicative Cotree

Functor Cotree

.value : Cotree a -> a

Totality: total
Visibility: public export

value : Cotree a -> a

Totality: total
Visibility: public export

.forest : Cotree a -> Inf (Coforest a)

Totality: total
Visibility: public export

forest : Cotree a -> Inf (Coforest a)

Totality: total
Visibility: public export

Coforest : Type -> Type

  A potentially finit stream of trees

Totality: total
Visibility: public export

singleton : a -> Cotree a

Totality: total
Visibility: public export

unfold : (b -> (a, Colist b)) -> b -> Cotree a

Totality: total
Visibility: public export

iterate : (a -> Colist a) -> a -> Cotree a

Totality: total
Visibility: public export

expand : (a -> Colist a) -> Cotree a -> Cotree a

Totality: total
Visibility: public export

fromTree : Tree a -> Cotree a

Totality: total
Visibility: public export

toTree : Nat -> Nat -> Cotree a -> Tree a

  Converts a Cotree to a tree of the given maximum depth and width.
  The maximum numbers of elements in the tree will be
  maxWidth ^ maxDepth.

Totality: total
Visibility: public export

mapCotree : (a -> b) -> Cotree a -> Cotree b

Totality: total
Visibility: public export

interleave : Cotree (a -> b) -> Cotree a -> Cotree b

Totality: total
Visibility: public export

bind : Cotree a -> (a -> Cotree b) -> Cotree b

Totality: total
Visibility: public export

bindMaybe : Cotree (Maybe a) -> (a -> Cotree (Maybe b)) -> Cotree (Maybe b)

Totality: total
Visibility: public export

shrink : Nat -> Cotree (Maybe a) -> List a

Totality: total
Visibility: public export

mapShrink : Nat -> (a -> Maybe b) -> Cotree a -> List b

Totality: total
Visibility: public export

shrinkIf : Nat -> (a -> Bool) -> Cotree a -> List a

Totality: total
Visibility: public export

pruneTo : Nat -> Nat -> Cotree a -> Cotree a

  Prunes a cotree up to the given depth and width.

Totality: total
Visibility: public export

prune : Cotree a -> Cotree a

  Removes all children from a cotree

Totality: total
Visibility: public export

takeUntil : (a -> Bool) -> Cotree a -> Cotree a

Totality: total
Visibility: public export

takeBeforeNothing : Cotree (Maybe a) -> Maybe (Cotree a)

Totality: total
Visibility: public export

takeBefore : (a -> Bool) -> Cotree a -> Maybe (Cotree a)

Totality: total
Visibility: public export

takeWhile : (a -> Bool) -> Cotree a -> Maybe (Cotree a)

Totality: total
Visibility: public export

mapMaybe : (a -> Maybe b) -> Cotree a -> Maybe (Cotree b)

Totality: total
Visibility: public export