Theorems · Definition · logic and foundations

Computable

{α : Type u_1} → {σ : Type u_2} → [Primcodable α] → [Primcodable σ] → (α → σ) → Prop

Computable functions α → σ between Primcodable types: a function is computable if and only if it is partially recursive (as a partial function)

Defined in

Mathlib.Computability.Partrec

Cited by

80 results in Mathlib

Foundations

Depth 11 from the axioms · uses no axioms

Assumes

PrimcodablePrimcodable