Lean4
/-- `Partrec f` means that the partial function `f : ℕ →. ℕ` is partially recursive. -/
inductive Partrec : (ℕ →. ℕ) → Prop
| zero : Partrec (pure 0)
| succ : Partrec succ
| left : Partrec ↑fun n : ℕ => n.unpair.1
| right : Partrec ↑fun n : ℕ => n.unpair.2
| pair {f g} : Partrec f → Partrec g → Partrec fun n => pair <$> f n <*> g n
| comp {f g} : Partrec f → Partrec g → Partrec fun n => g n >>= f
|
prec {f g} :
Partrec f →
Partrec g →
Partrec
(unpaired fun a n =>
n.rec (f a) fun y IH => do
let i ← IH;
g (pair a (pair y i)))
| rfind {f} : Partrec f → Partrec fun a => rfind fun n => (fun m => m = 0) <$> f (pair a n)
