Confusion about `Order.isSuccLimitRecOn`

Stream: mathlib4

[Aaron Liu]

I am trying to define something on ordinals by induction. I decided to use docs#Order.isSuccLimitRecOn. I quickly noticed that this theorem doesn't give me access to any induction hypotheses, and what I was actually looking for was docs#SuccOrder.limitRecOn. Should Order.isSuccLimitRecOn be renamed to Order.isSuccLimitCasesOn, to reflect that it doesn't give you access to any induction hypotheses?

[Kenny Lau]

@Aaron Liu according to @Violeta Hernández , using the rec is a beginner's trap, and you should use decreasing_by recursion instead

[Aaron Liu]

why is it a beginner's trap

[Aaron Liu]

is this bad

[Kenny Lau]

but actually the Ordinal rec you want is Ordinal.limitRecOn

[Kenny Lau]

because most of the time you actually don't need the base cases for limitRecOn

[Aaron Liu]

this time I do need the zero base case

[Aaron Liu]

I could rewrite it to not use that but

[Aaron Liu]

Kenny Lau said:

but actually the Ordinal rec you want is Ordinal.limitRecOn

I'm actually using NatOrdinal from CombinatorialGames (which was downstreamed from the docs#NatOrdinal in mathlib)

[Violeta Hernández]

a) I didn't say docs#SuccOrder.limitRecOn was a noob trap, I said that the technique of limit induction itself is; at least in most cases I've seen, you can replace constructions through limit induction or recursion by simpler constructions using only well-founded induction. But most doesn't mean all!
b) I agree it's weird for the namespaces to be distinct, I think that should be changed.
c) You should probably create NatOrdinal.limitRecOn for what you're doing; it would be def-eq to the ordinal theorem but of course be stated in terms of the type alias.