Commit 2025-11-24 06:51 c1ee2821

refactor: make Nat.digits use well-founded recursion once again (#30246) #25864 made Nat.digits structurally recursive, which has some benefits. In doing so, however, it added significant complexity. As brought up in this zulip thread, on the balance that PR might not be considered an improvement. The present PR reverts that change (but keeps a code golf that was bundled with it). Note that recent improvements to core Lean mean that simp can handle the structurally recursive version without a problem:

example : digits 10 123456789 = [9,8,7,6,5,4,3,2,1] := by
  simp [digits, digitsAux]