α : Type u_1
β : Type u_3
γ : Type ?u.126196
δ : Type ?u.126199
σ : Type u_2
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f
α : Type u_1
β : Type u_3
γ : Type ?u.126196
δ : Type ?u.126199
σ : Type u_2
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.map (f a) (decode n)) ↔ Primrec₂ f
simp only [Option.map_eq_bind]
no goals
α : Type u_1
β : Type u_3
γ : Type ?u.126196
δ : Type ?u.126199
σ : Type u_2
inst✝⁴ : Primcodable α
inst✝³ : Primcodable β
inst✝² : Primcodable γ
inst✝¹ : Primcodable δ
inst✝ : Primcodable σ
f : α → β → σ
⊢ (Primrec₂ fun a n => Option.bind (decode n) (some ∘ f a)) ↔ Primrec₂ f
exact bind_decode_iff.trans Primrec₂.option_some_iff