Theorems · Definition · logic and foundations

PrimrecPred

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

PrimrecPred p means p : α → Prop is a primitive recursive predicate, which is to say that decide ∘ p : α → Bool is primitive recursive.

Defined in

Mathlib.Computability.Primrec.Basic

Cited by

23 results in Mathlib

Foundations

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

Assumes

Primcodable