BinaryTree

Persistent, labelled binary trees; no ordering invariant is imposed.
Table of Contents

Types

BinaryTree

(inductive)
Persistent, labelled binary trees; no ordering invariant is imposed.
inductive BinaryTree a

Constructors

For each type in this module: inductive types list their declared constructors; opaque types list any local function whose name starts with mk and which returns a value of that type.

BinaryTree (inductive)

leaf

constructor
(BinaryTree a)

node

constructor
(BinaryTree a)

Functions

map

def map (f : (x : a) → b) (tree : (BinaryTree a)) : (BinaryTree b)

fold

def fold (z : b) (f : (left : b) → (x : a) → (right : b) → b) (tree : (BinaryTree a)) : b