Theorems · Definition · logic and foundations

RecursiveIn

{α : Type u_5} → {σ : Type u_6} → [Primcodable α] → [Primcodable σ] → Set (ℕ →. ℕ) → (α →. σ) → Prop

A partial function f : α →. σ between Primcodable types is recursive in a set of oracles O if its encoding as a function ℕ →. ℕ is Nat.RecursiveIn O.

Defined in

Mathlib.Computability.RecursiveIn

Cited by

15 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable