tree

Tree

data Tree (A : Type)

A binary tree with values of A at its nodes.

Tree.size

def size {A : Type} (t : Tree A) : Nat

The number of nodes.

Tree.leafCount

def leafCount {A : Type} (t : Tree A) : Nat

The number of leaves (one more than the nodes).

Tree.depth

def depth {A : Type} (t : Tree A) : Nat

The number of nodes on the longest path from the root to a leaf.

Tree.map

def map {A : Type} {B : Type} (f : A -> B) (t : Tree A) : Tree B

f applied to every value, the shape kept.

Tree.mirror

def mirror {A : Type} (t : Tree A) : Tree A

The subtrees swapped at every node.

Tree.zip

def zip {A : Type} {B : Type} (a : Tree A) (b : Tree B) : Tree (A * B)

The pairs of values where both trees have a node.

Tree.fold

def fold {A : Type} {B : Type} (atLeaf : B) (f : A -> B -> B -> B) (t : Tree A) : B

The values from the leaves up: atLeaf at each leaf, f x left right at each node.

Tree.inorder

def inorder {A : Type} (t : Tree A) : List A

The values in order: the left subtree, the node, the right subtree.

Tree.preorder

def preorder {A : Type} (t : Tree A) : List A

The values with each node before its subtrees.

Tree.postorder

def postorder {A : Type} (t : Tree A) : List A

The values with each node after its subtrees.

Tree.all

def all {A : Type} (test : A -> Bool) (t : Tree A) : Bool

Whether every value passes the test.

Tree.any

def any {A : Type} (test : A -> Bool) (t : Tree A) : Bool

Whether some value passes the test.

Tree.root

def root {A : Type} (t : Tree A) : Option A

The value at the root, if the tree is a node.

Tree.leftSubtree

def leftSubtree {A : Type} (t : Tree A) : Tree A

The left subtree of a node; a leaf’s is a leaf.

Tree.rightSubtree

def rightSubtree {A : Type} (t : Tree A) : Tree A

The right subtree of a node; a leaf’s is a leaf.

Tree.insertLeft

def insertLeft {A : Type} (x : A) (t : Tree A) : Tree A

A new node with x at the leftmost leaf.

Tree.insertRight

def insertRight {A : Type} (x : A) (t : Tree A) : Tree A

A new node with x at the rightmost leaf.

Tree.mapIdentity

def mapIdentity {A : Type} (t : Tree A) : map (fun (x : A) => x) t = t

Mapping the identity changes nothing.

Tree.mapCompose

def mapCompose {A : Type} {B : Type} {C : Type} (f : A -> B) (g : B -> C) (t : Tree A) : map g (map f t) = map (fun (x : A) => g (f x)) t

Mapping twice is mapping the composition.

Tree.sizeMap

def sizeMap {A : Type} {B : Type} (f : A -> B) (t : Tree A) : size (map f t) = size t

Mapping keeps the size.

Tree.mirrorMirror

def mirrorMirror {A : Type} (t : Tree A) : mirror (mirror t) = t

Mirroring twice gives the tree back.

Tree.sizeMirror

def sizeMirror {A : Type} (t : Tree A) : size (mirror t) = size t

Mirroring keeps the size.

Tree.depthMirror

def depthMirror {A : Type} (t : Tree A) : depth (mirror t) = depth t

Mirroring keeps the depth.

Tree.mirrorMap

def mirrorMap {A : Type} {B : Type} (f : A -> B) (t : Tree A) : mirror (map f t) = map f (mirror t)

Mirroring and mapping commute.