Theorems · Theorem · logic and foundations

Primrec.nat_strong_rec

∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] (f : α → ℕ → σ)
  {g : α → List σ → Option σ},
  Primrec₂ g → (∀ (a : α) (n : ℕ), g a (List.map (f a) (List.range n)) = some (f a n)) → Primrec₂ f

Defined in

Mathlib.Computability.Primrec.List

Cited by

2 results in Mathlib

Foundations

Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PrimcodablePrimcodable