case refine'_2
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' fun v => Part.some (Vector.get v i)
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i : Fin (n + 1)
⊢ Partrec' ((fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i) i)
refine' Fin.cases _ (fun i => _) i <;> simp [*]
no goals
case refine'_2
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
i✝ : Fin (n + 1)
i : Fin n
⊢ Partrec' fun v => Part.some (Vector.get v i)
exact prim (Nat.Primrec'.get _)
no goals
n : ℕ
f : Vector ℕ n →. ℕ
g : Vector ℕ (n + 1) →. ℕ
hf : Partrec' f
hg : Partrec' g
v : Vector ℕ n
⊢ (mOfFn fun i => Fin.cases f (fun i v => ↑(some (Vector.get v i))) i v) >>= g = Part.bind (f v) fun a => g (a ::ᵥ v)
simp [mOfFn, Part.bind_assoc, pure]