@[reducible, inline]

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

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

Equations

• List.Encoding A = ((n : ℕ) × (Fin n → A))

def List.Encoding.nil {A : Type u_1} : Encoding A

The encoded version of [].

Equations

• List.Encoding.nil = ⟨0, Fin.elim0⟩

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

The encoded version of · ∷ ·.

Equations

• List.Encoding.cons x xs = ⟨xs.fst + 1, fun (i : Fin (xs.fst + 1)) => Fin.cases x xs.snd i⟩

@[irreducible]

def List.Encoding.foldr {A : Type u_1} {B : Type u_2} (cons : A → B → B) (nil : B) : Encoding A → B

The encoded version of List.foldr.

Equations

• List.Encoding.foldr cons nil ⟨0, snd⟩ = nil
• List.Encoding.foldr cons nil ⟨n.succ, k⟩ = cons (k 0) (List.Encoding.foldr cons nil ⟨n, fun (i : Fin n) => k i.succ⟩)

@[simp]

theorem List.Encoding.foldr_nil {A : Type u_4} {B : Type u_5} (f : A → B → B) (z : B) : foldr f z nil = z

@[simp]

theorem List.Encoding.foldr_cons {A : Type u_4} {B : Type u_5} (f : A → B → B) (z : B) (x : A) (xs : Encoding A) : foldr f z (cons x xs) = f x (foldr f z xs)

@[simp]

theorem List.Encoding.nil_ne_cons {A : Type u_1} (x : A) (xs : Encoding A) : nil ≠ cons x xs

@[simp]

theorem List.Encoding.cons_ne_nil {A : Type u_1} (x : A) (xs : Encoding A) : cons x xs ≠ nil

@[simp]

theorem List.Encoding.cons_inj_iff {A : Type u_1} (x y : A) (xs ys : Encoding A) : cons x xs = cons y ys ↔ x = y ∧ xs = ys

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

Encodes a List A as an Encoding A.

Equations

• List.Encoding.encode = List.foldr List.Encoding.cons List.Encoding.nil

@[simp]

theorem List.Encoding.encode_nil {A : Type u_4} : encode [] = nil

@[simp]

theorem List.Encoding.encode_cons {A : Type u_4} (x : A) (xs : List A) : encode (x :: xs) = cons x (encode xs)

@[simp]

theorem List.Encoding.encode_injective {A : Type u_1} : Function.Injective encode