RoseTree

Ordered trees with an arbitrary number of children. Empty trees are explicit.
Imports
open Seq;
Table of Contents

Types

RoseTree

(inductive)
inductive RoseTree 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.

RoseTree (inductive)

empty

constructor
(RoseTree a)

node

constructor
(RoseTree a)

Functions

map

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

fold

def fold (z : b) (f : (x : a) → (children : (Seq b)) → b) (tree : (RoseTree a)) : b