Theorems · Definition · logic and foundations

PrimrecRel

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

PrimrecRel p means p : α → β → Prop is a primitive recursive relation, which is to say that decide ∘ p : α → β → Bool is primitive recursive.

Defined in

Mathlib.Computability.Primrec.Basic

Cited by

22 results in Mathlib

Foundations

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

Assumes

PrimcodablePrimcodable