α : Type u_1
β : Type ?u.365224
γ : Type ?u.365227
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => f 0 a :: List.ofFn fun i => f (Fin.succ i) a
α : Type u_1
β : Type ?u.365224
γ : Type ?u.365227
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => List.ofFn fun i => f i a
simp [List.ofFn_succ]
no goals
α : Type u_1
β : Type ?u.365224
γ : Type ?u.365227
σ : Type u_2
inst✝³ : Primcodable α
inst✝² : Primcodable β
inst✝¹ : Primcodable γ
inst✝ : Primcodable σ
n : ℕ
f : Fin (n + 1) → α → σ
hf : ∀ (i : Fin (n + 1)), Primrec (f i)
⊢ Primrec fun a => f 0 a :: List.ofFn fun i => f (Fin.succ i) a
exact list_cons.comp (hf 0) (list_ofFn fun i => hf i.succ)