Forests

Rooted forests with preorder and postorder traversals.

inductive Forest (α : Type u_1) : Type u_1

• nil {α : Type u_1} : Forest α
• node {α : Type u_1} (a : α) (child sibling : Forest α) : Forest α

def instReprForest.repr {α✝ : Type u_1} [Repr α✝] : Forest α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprForest.repr Forest.nil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Forest.nil")).group prec✝

@[instance_reducible]

instance instReprForest {α✝ : Type u_1} [Repr α✝] : Repr (Forest α✝)

Equations

• instReprForest = { reprPrec := instReprForest.repr }

def Forest.roots {α : Type u_1} (f : Forest α) : Set α

Equations

• Forest.nil.roots = ∅
• (Forest.node a child s).roots = insert a s.roots

def Forest.support {α : Type u_1} (f : Forest α) : Set α

Equations

• Forest.nil.support = ∅
• (Forest.node a child s).support = insert a (child.support ∪ s.support)

theorem Forest.roots_subset_support {α : Type u_1} (f : Forest α) : f.roots ⊆ f.support

def Forest.pre {α : Type u_1} (f : Forest α) : List α

Equations

• Forest.nil.pre = ∅
• (Forest.node a child s).pre = a :: child.pre ++ s.pre

def Forest.post {α : Type u_1} (f : Forest α) : List α

Equations

• Forest.nil.post = ∅
• (Forest.node a child s).post = child.post ++ a :: s.post

def Forest.append {α : Type u_1} (f g : Forest α) : Forest α

Equations

• Forest.nil.append g = g
• (Forest.node a child s).append g = Forest.node a child (s.append g)

@[instance_reducible]

instance Forest.instAppend {α : Type u_1} : Append (Forest α)

Equations

• Forest.instAppend = { append := Forest.append }