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)

Estimated changes

modified theorem Primrec.nat_findGreatest
modified theorem Primrec.option_guard
added theorem Primrec.primrecPred
deleted theorem PrimrecPred.and
modified theorem PrimrecPred.comp
modified theorem PrimrecPred.exists_mem_list
modified theorem PrimrecPred.forall_mem_list
deleted theorem PrimrecPred.not
modified theorem PrimrecPred.of_eq
deleted theorem PrimrecPred.or
added theorem PrimrecPred.primrecRel
modified def PrimrecPred
modified theorem PrimrecRel.comp
modified theorem PrimrecRel.comp₂
modified theorem PrimrecRel.listFilter
modified def PrimrecRel
added theorem Primrec₂.primrecRel
deleted theorem Primrec₂.swap