theorem List.lookup_map_fun_of_mem {β : Type u_2} {α : Type u} [DecidableEq α] (f : α → β) {a : α} {as : List α} (h : a ∈ as) : List.lookup a (List.map (fun (x : α) => (x, f x)) as) = some (f a)

def List.mapGraph {β : Type u_2} {α : Type u} [DecidableEq α] (M : List (α × β)) (as : List α) : List β

Equations

• M.mapGraph as = as.bind fun (x : α) => (List.lookup x M).toList

theorem List.mapGraph_graph {β : Type u_2} {α : Type u} [DecidableEq α] (f : α → β) {as : List α} {as' : List α} (has : as' ⊆ as) : (List.map (fun (x : α) => (x, f x)) as).mapGraph as' = List.map f as'

theorem List.subset_bind_of_mem {α : Type u} {a : α} {as : List α} (h : a ∈ as) (f : α → List α) : f a ⊆ as.bind f

theorem Primrec.nat_rec'' {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : α → ℕ} {g : α → β} {h : α → ℕ → β → β} (hf : Primrec f) (hg : Primrec g) (hh : Primrec₂ fun (a : α) (p : ℕ × β) => h a p.1 p.2) : Primrec fun (a : α) => Nat.rec (g a) (h a) (f a)

theorem Primrec.option_toList {α : Type u_1} [Primcodable α] : Primrec Option.toList

theorem Primrec.iterate {α : Type u_1} [Primcodable α] {f : α → α} (hf : Primrec f) : Primrec₂ fun (x : ℕ) (x_1 : α) => f^[x] x_1

theorem Primrec.list_take {α : Type u_1} [Primcodable α] : Primrec₂ List.take

theorem Primrec.nat_pow : Primrec₂ fun (x x_1 : ℕ) => x ^ x_1

theorem Primrec.list_lookup {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [DecidableEq α] : Primrec₂ List.lookup

theorem Primrec.list_mapGraph {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] [DecidableEq α] : Primrec₂ List.mapGraph

theorem Primrec.nat_omega_rec_prod {α : Type u_1} {σ : Type u_4} [Primcodable α] [Primcodable σ] [DecidableEq α] {t : α → ℕ → α} (f : α → ℕ → σ) {g : α × ℕ → List σ → Option σ} (ht : Primrec₂ t) (hg : Primrec₂ g) (H : ∀ (a : α) (k : ℕ), g (a, k) (List.map (f (t a k)) (List.range k)) = some (f a k)) : Primrec₂ f