exact Partrec'.rfind hf
n : ℕ
f✝ : Vector ℕ n →. ℕ
n✝ : ℕ
f : Vector ℕ (n✝ + 1) → ℕ
a✝ : ArithPart₁ ↑f
hf : Partrec' ↑f
⊢ Partrec' fun v => Nat.rfind fun n => Part.some (decide (f (n ::ᵥ v) = 0))
no goals