no goals
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i : Fin (succ m)
⊢ Partrec' fun v => ↑(some (Vector.get ((fun v => f v ::ᵥ g v) v) 0))
simpa using hf
no goals
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Partrec' ↑f
hg : Vec g
i✝ : Fin (succ m)
i : Fin m
⊢ Partrec' fun v => ↑(some (Vector.get ((fun v => f v ::ᵥ g v) v) (Fin.succ i)))
simp only [hg i, get_cons_succ]