Mathlib computability lemmas all report Classical.choice

Audit with #print axioms on Mathlib v4.35: Nat.Partrec.Code.evaln_mono, evaln_sound, evaln_complete, exists_code, eval_curry, primrec_evaln, Primrec.nat_iff and ComputablePred.halting_problem all depend on [propext, Classical.choice, Quot.sound]. Denumerable.ofNat_encode uses only propext and Quot.sound, and Nat.rfind_spec uses no axioms. As a result, any downstream result in computability (even monotonicity facts about a primitive recursive evaluator, or prefix-closure of a concrete tree) reports Classical.choice, and #print axioms cannot tell you whether a computability theorem is constructive. If you need choice-free results, plan on re-proving the evaln lemmas, and avoid simp/omega closers that pull in classical Decidable instances.