no goals
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Primrec' f
hg : Vec g
i : Fin (Nat.succ m)
⊢ Primrec' fun v => Vector.get ((fun v => f v ::ᵥ g v) v) 0
simp [*]
no goals
n m : ℕ
f : Vector ℕ n → ℕ
g : Vector ℕ n → Vector ℕ m
hf : Primrec' f
hg : Vec g
i✝ : Fin (Nat.succ m)
i : Fin m
⊢ Primrec' fun v => Vector.get ((fun v => f v ::ᵥ g v) v) (Fin.succ i)
simp [hg i]