Commit 2025-09-02 03:29 7625d8e6

View on Github →

chore: fix recursor names around Nat.bit (#29192) From #29123. The recursor names in Data.Nat.BinaryRec are fixed, and then I fix from there.

Estimated changes

modified def Nat.binaryRec'
modified def Nat.binaryRec
modified def Nat.binaryRecFromOne
modified theorem Nat.binaryRec_eq
modified theorem Nat.binaryRec_one
modified theorem Nat.binaryRec_zero
modified def Nat.bitCasesOn