Commit 2026-10-27 23:51 69552756

View on Github →

chore(Data/Nat/Init): rename recursor arguments (#43848) Name the motive motive and name the minor premises according to their contents.

Estimated changes

modified theorem Nat.diag_induction
modified def Nat.leRecOn
modified theorem Nat.leRecOn_self
modified theorem Nat.leRecOn_succ'
modified theorem Nat.leRecOn_succ
modified theorem Nat.leRecOn_succ_left
modified theorem Nat.leRecOn_trans
modified theorem Nat.le_induction
modified def Nat.pincerRecursion
modified theorem Nat.rec_add_one
modified theorem Nat.rec_one
modified theorem Nat.rec_zero