Data.Tree

Definitions

record Tree : Type -> Type

  A finite rose tree

Totality: total
Visibility: public export
Constructor: 

MkTree : a -> Forest a -> Tree a

Projections:

.forest : Tree a -> Forest a

.value : Tree a -> a

Hints:

Applicative Tree

Eq a => Eq (Tree a)

Foldable Tree

Functor Tree

Monad Tree

Traversable Tree

.value : Tree a -> a

Totality: total
Visibility: public export

value : Tree a -> a

Totality: total
Visibility: public export

.forest : Tree a -> Forest a

Totality: total
Visibility: public export

forest : Tree a -> Forest a

Totality: total
Visibility: public export

Forest : Type -> Type

  A finite forest of trees

Totality: total
Visibility: public export

singleton : a -> Tree a

Totality: total
Visibility: public export

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

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

Totality: total
Visibility: public export

layers : Tree a -> List (List a)

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

drawTree : Tree String -> String

Totality: total
Visibility: export