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 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 a_1 a_2).roots = insert a a_2.roots

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

Equations

• Forest.nil.support = ∅
• (Forest.node a a_1 a_2).support = insert a (a_1.support ∪ a_2.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 a_1 a_2).pre = a :: a_1.pre ++ a_2.pre

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

Equations

• Forest.nil.post = ∅
• (Forest.node a a_1 a_2).post = a_1.post ++ a :: a_2.post

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

Equations

• Forest.nil.append g = g
• (Forest.node a a_1 a_2).append g = Forest.node a a_1 (a_2.append g)

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

Equations

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