n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.bind (f v) (Part.some ∘ fun a => g (a ::ᵥ v))
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.map (fun a => g (a ::ᵥ v)) (f v)
simp [(Part.bind_some_eq_map _ _).symm]
no goals
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) → ℕ
hf : Partrec' f
hg : Partrec' ↑g
⊢ Partrec' fun v => Part.bind (f v) (Part.some ∘ fun a => g (a ::ᵥ v))
exact hf.bind hg