LeanPool.QuasiBorelSpaces.Rose.Encoding

Imported Lean Pool material for LeanPool.QuasiBorelSpaces.Rose.Encoding.

@[reducible, inline]

abbrev Rose.Encoding (A : Type u_4) : Type u_4

We derive the QuasiBorelSpace instance for Rose As from their encoding as (_ : Rose Unit) × (List ℕ → A).

Equations

• Rose.Encoding A = ((_ : Rose Unit) × (List ℕ → A))

def Rose.Encoding.mk {A : Type u_1} (x : A) (xs : List (Encoding A)) : Encoding A

The encoded version of Rose.mk.

Equations

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

@[irreducible]

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

The encoded version of Rose.foldr.

Equations

• Rose.Encoding.fold mk ⟨{ label := PUnit.unit, children := xs }, k⟩ = mk (k []) (List.ofFn fun (i : Fin xs.length) => Rose.Encoding.fold mk ⟨xs[i], fun (is : List ℕ) => k (↑i :: is)⟩)

@[simp]

theorem Rose.Encoding.fold_mk {A : Type u_1} {B : Type u_2} (f : A → List B → B) (x : A) (xs : List (Encoding A)) : fold f (mk x xs) = f x (List.map (fold f) xs)

def Rose.Encoding.encode {A : Type u_1} : Rose A → Encoding A

Encodes a Rose A as an Encoding A.

Equations

• Rose.Encoding.encode = Rose.fold Rose.Encoding.mk

@[simp]

theorem Rose.Encoding.encode_mk {A : Type u_1} (x : A) (xs : List (Rose A)) : encode { label := x, children := xs } = mk x (List.map encode xs)