def finEncodingListBool : Computability.FinEncoding (List Bool)

Equations

• finEncodingListBool = { Γ := Bool, encode := id, decode := some, decode_encode := finEncodingListBool._proof_1, ΓFin := Bool.fintype }

@[simp]

theorem splitOnP_isNone_map_some {α : Type} (l : List α) : List.splitOnP Option.isNone (List.map some l) = [List.map some l]

@[simp]

theorem splitOnP_append_cons {α : Type} (l1 l2 : List α) (a : α) (P : α → Bool) (hPa : P a = true) : List.splitOnP P (l1 ++ a :: l2) = List.splitOnP P l1 ++ List.splitOnP P l2

@[simp]

theorem Option.getD_comp_some : (fun (x : Option Bool) => x.getD false) ∘ some = id

def finEncodingListBoolProdListBool : Computability.FinEncoding (List Bool × List Bool)

Equations

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