Data.Container.Base.TreeUtils

Definitions

data BinTreeShape : Type

  Shapes of binary trees

Totality: total
Visibility: public export
Constructors:

LeafS : BinTreeShape

NodeS : BinTreeShape -> BinTreeShape -> BinTreeShape

Hints:

DecEq (BinTreePos b)

DecEq (BinTreePosNode b)

DecEq (BinTreePosLeaf b)

Eq BinTreeShape

Eq (BinTreePos b)

Eq (BinTreePosNode b)

Eq (BinTreePosLeaf b)

Finite (BinTreePosNode b)

Finite (BinTreePosLeaf b)

MOrd (BinTreePos b)

MOrd (BinTreePosNode b)

MOrd (BinTreePosLeaf b)

Show BinTreeShape

Show (BinTreePos b)

Show (BinTreePosNode b)

Show (BinTreePosLeaf b)

numLeaves : BinTreeShape -> Nat

Totality: total
Visibility: public export

numNodes : BinTreeShape -> Nat

Totality: total
Visibility: public export

numNodesAndLeaves : BinTreeShape -> Nat

Totality: total
Visibility: public export

data BinTreePos : BinTreeShape -> Type

  Positions corresponding to both nodes and leaves within a BinTreeShape

Totality: total
Visibility: public export
Constructors:

AtLeaf : BinTreePos LeafS

AtNode : BinTreePos (NodeS l r)

GoLeft : BinTreePos l -> BinTreePos (NodeS l r)

GoRight : BinTreePos r -> BinTreePos (NodeS l r)

Hints:

DecEq (BinTreePos b)

Eq (BinTreePos b)

MOrd (BinTreePos b)

Show (BinTreePos b)

data BinTreePosNode : BinTreeShape -> Type

  Positions corresponding to nodes within a BinTreeNode shape.

Totality: total
Visibility: public export
Constructors:

AtNode : BinTreePosNode (NodeS l r)

GoLeft : BinTreePosNode l -> BinTreePosNode (NodeS l r)

GoRight : BinTreePosNode r -> BinTreePosNode (NodeS l r)

Hints:

DecEq (BinTreePosNode b)

Eq (BinTreePosNode b)

Finite (BinTreePosNode b)

MOrd (BinTreePosNode b)

Show (BinTreePosNode b)

data BinTreePosLeaf : BinTreeShape -> Type

  Positions corresponding to leaves within a BinTreeShape 

Totality: total
Visibility: public export
Constructors:

AtLeaf : BinTreePosLeaf LeafS

GoLeft : BinTreePosLeaf l -> BinTreePosLeaf (NodeS l r)

GoRight : BinTreePosLeaf r -> BinTreePosLeaf (NodeS l r)

Hints:

DecEq (BinTreePosLeaf b)

Eq (BinTreePosLeaf b)

Finite (BinTreePosLeaf b)

MOrd (BinTreePosLeaf b)

Show (BinTreePosLeaf b)