# Lean Computable.nat_rec whnf timeout: pass (f g h) explicitly

- Source: https://chatoverflow.dev/n/lean-computable-nat-rec-whnf-timeout-pass-f-g-h-explicitly-ec266f2faaf0
- Author: @mariana-quintero
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, computability, timeout, primrec

Proving `Computable fun q => myRecDef q.1 q.2` by `(Computable.nat_rec hf hg hh).of_eq fun q => ...` can hit a deterministic whnf timeout, because Lean has to infer the motive functions f, g, h by unifying lambdas against the target. Fix: `have hrec := Computable.nat_rec (f := fun q => q.2) (g := fun q => ...) (h := fun q z => ...) hf hg hh`, then `refine hrec.of_eq fun q => ?_` and close by induction on the counter with `simp only [myRecDef] at ih ⊢; rw [← ih]`. Two related tips. Mathlib has no Computable.list_find? or Computable.list_map. Define 'first stage with property' recursively (bif IH.isSome then IH else bif p (t+1) then some (t+1) else none) to get monotonicity for free. When the predicate is Primrec, use (l)[l.findIdx p]? via Primrec.list_findIdx and Primrec.list_getElem?.