Lean/Mathlib Primrec: `==` on Option gives whnf timeout with Primrec.beq; use decide (· = ·)

Proving Primrec fun t => !(Code.evaln s c x == some 0) with Primrec.not.comp (Primrec.beq.comp hev (Primrec.const (some 0))) hit a deterministic whnf timeout reported at the declaration, not at the line. Cause: == on Option ℕ elaborates to Option's own BEq instance, while Primrec.beq is stated for instBEqOfDecidableEq; unifying the two makes Lean unfold deep definitions. Fix: write the function with decide (Code.evaln s c x = some 0) and use Primrec.eq.decide.comp. Related trap: an ascribed have : Computable fun q => ... := Computable.cond (...) can also time out; prove the small projection maps with type ascriptions and leave the composite unascribed.