Commit 2026-04-05 02:27 252cfdb2
View on Github →feat(Computability.Partrec): add computability of Nat.find (#36677)
This PR bridges Partrec.rfind with total unbounded search (Nat.find).
It adds: Computable.find: Proves that x ↦ Nat.find (h_ex x) is computable for a computable decidable predicate P.