NoMaxOrder.infinite

Stream: mathlib4

[Violeta Hernández]

The docstring says this isn't an instance to avoid a cycle. But in Lean 4 this shouldn't be an issue anymore, right?

[Violeta Hernández]

docs#NoMaxOrder.infinite

[Anne Baanen]

Yes, in Lean 4 the rule is that cycles are allowed as long as literally the same thing appears when the cycle completes. So indeed Infinite α → Nontrivial α → Nonempty α → Infinite α should be okay to add. But for example, we couldn't allow the implication Nonempty (α × β) → Nonempty α as an instance.

[Kevin Buzzard]

Oh thank you for the loop explanation Anne! I remembered from years ago the claim that in lean 4 TC loops would be allowed, but sometimes when I'd tried them they had caused problems and I had incorrectly concluded that the original claim had been dropped somehow.

[Violeta Hernández]

#18456

[Jireh Loreaux]

Yes, this is very enlightening. Thanks!