inductive Forest (α : Type u_1) : Type u_1

• nil: {α : Type u_1} → Forest α
• node: {α : Type u_1} → α → Forest α → Forest α → Forest α

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

Equations

• instReprForest = { reprPrec := reprForest✝ }

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 : Forest α) (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 }