Data.Tree

(source)

Finite Rose Trees

Definitions

record Tree : Type -> Type

  A finite rose tree

Totality: total
Visibility: public export
Constructor:

T : a -> List (Tree a) -> Tree a

Projections:

.forest : Tree a -> List (Tree a)
.value : Tree a -> a

Hints:

Applicative Tree
Eq a => Eq (Tree a)
Foldable Tree
Functor Tree
Monad Tree
Show a => Show (Tree a)
Traversable Tree

.value : Tree a -> a

Totality: total
Visibility: public export

value : Tree a -> a

Totality: total
Visibility: public export

.forest : Tree a -> List (Tree a)

Totality: total
Visibility: public export

forest : Tree a -> List (Tree a)

Totality: total
Visibility: public export

Forest : Type -> Type

  A finite forest of trees

Totality: total
Visibility: public export

singleton : a -> Tree a

  Wrap a single value in a tree

Totality: total
Visibility: public export

replicate : Nat -> Nat -> a -> Tree a

  Create a regular tree of the given depth, where each branch has
  `width` children.

Totality: total
Visibility: public export

unfold : Nat -> (s -> (a, List s)) -> s -> Tree a

  Unfold a tree up to the given depth.

Totality: total
Visibility: public export

flatten : Tree a -> List a

  Flatten a tree into a list.

Totality: total
Visibility: public export

layers : Tree a -> List (List a)

  Convert a tree to a list of lists, so that all values at the same
  depth appear in the same list.

Totality: total
Visibility: public export

index : List Nat -> Tree a -> Maybe a

  Try to look up a value in the tree by following the given path.

Totality: total
Visibility: public export

drawTree : Tree String -> String

  Pretty print a tree.
  
  Unlike `prettyTree`, this has support for multi-line strings and
  will result in a vertically elongated representation.

Totality: total
Visibility: export

prettyTree : Bool -> Tree String -> String

  Pretty print a tree.
  
  Unlike `drawTree`, this does not work with multi-line node labels,
  but will otherwise result in a vertically more compact representation.
  In addition, it is possible to print the tree "upside-down" by
  setting `rev` to `True`.

Totality: total
Visibility: export