Commit 2025-11-27 09:46 a3c69a18

View on Github →

feat(Data/Nat): reducible strong recursion (#30181)

Redefine Nat.strongRec' to allow Lean kernel computation (reduction) with the strong Nat recursor. TODO: maybe merge this with Batteries' Nat.strongRec.
Redefine Nat.xgcd to use Nat.strongRec' to allow kernel reduction.

Estimated changes

Modified Mathlib/Data/Int/GCD.lean

modified theorem Nat.gcdA_zero_left

modified theorem Nat.gcdB_zero_left

modified def Nat.xgcdAux

modified theorem Nat.xgcd_zero_left

Modified Mathlib/Data/Nat/Init.lean

added theorem Nat.strongRec'_spec

modified def Nat.strongRecOn'