LeanPool.QuasiBorelSpaces.RoseTree.Defs

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.RoseTree.Defs.

structure Rose (A : Type u) : Type u

The type of node-labelled, finitely branching trees.

• label : A

  The label of the root node.

• children : List (Rose A)

  The list of child trees.

@[irreducible]

def Rose.fold {A : Type u_1} {B : Type u_2} (f : A → List B → B) : Rose A → B

The fold operation over trees.

Equations

• Rose.fold f { label := x_1, children := xs } = f x_1 (List.map (Rose.fold f) xs)

@[irreducible]

def Rose.bind {A : Type u_1} {B : Type u_2} (f : A → Rose B) : Rose A → Rose B

Grafts a tree to every sub-node in a Rose tree.

Equations

• Rose.bind f { label := x_1, children := xs } = { label := (f x_1).label, children := (f x_1).children ++ List.map (Rose.bind f) xs }

def Rose.map {A : Type u_1} {B : Type u_2} (f : A → B) : Rose A → Rose B

Applies a function to every label in a Rose tree.

Equations

• Rose.map f = Rose.bind fun (x : A) => { label := f x, children := [] }

@[implicit_reducible]

instance Rose.instMonad : Monad Rose

Equations

• One or more equations did not get rendered due to their size.

@[irreducible]

def Rose.encode {A : Type u_1} [Encodable A] : Rose A → ℕ

An injection into the natural numbers.

Equations

• { label := x_1, children := xs }.encode = Nat.pair (Encodable.encode x_1) (Encodable.encode (List.map Rose.encode xs))

@[irreducible]

def Rose.decode {A : Type u_1} [Encodable A] (n : ℕ) : Option (Rose A)

The inverse of encode.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Rose.instLE {A : Type u_1} [LE A] : LE (Rose A)

Equations

• Rose.instLE = { le := Rose.fold fun (x : A) (rec : List (Rose A → Prop)) (t : Rose A) => x ≤ t.label ∧ List.Forall₂ id rec t.children }