Naming of `Int` recursors

Stream: mathlib4

[Jeremy Tan]

https://github.com/leanprover-community/mathlib4/pull/25512#discussion_r2132112154 @Eric Wieser said that the induction principles for Int need better names than their current hz, hp, hn. But I am pretty sure those names are defined in core, but I can't find the exact location

[Eric Wieser]

show_term will find it for you

[Jeremy Tan]

/poll What should the new recursor names be?
zero, pos, neg
zero, toNat, negSucc

[Notification Bot]

This topic was moved here from #lean4 > Naming of `Int` recursors by Eric Wieser.

[Aaron Liu]

Found it, it's docs#Int.induction_on

[Jeremy Tan]

I opened a poll on the better names above

[Jeremy Tan]

wait, so it's in mathlib after all...

[Jeremy Tan]

#25555 fixes the branch names to zero, succ, pred