Commit 2025-08-22 16:06 825c937c
View on Github →refactor: don't require DecidablePred
to state PrimrecPred
(#27076)
def PrimrecPred {α} [Primcodable α] (p : α → Prop) [DecidablePred p] :=
Primrec fun a => decide (p a)
Currently, DecidablePred
is required to state PrimrecPred
, so this PR changes the definition and adds convenient APIs for this new definition:
def PrimrecPred {α} [Primcodable α] (p : α → Prop) :=
∃ (_ : DecidablePred p), Primrec fun a => decide (p a)