Mutual recursion

Stream: general

[Violeta Hernández]

I remember seeing the keyword mutual once, which caught me completely off guard. I understand that it can be used for "mutual induction" but I don't know if that means what I think it means

[Violeta Hernández]

How does this work?

[Violeta Hernández]

I'm interested in it because it might lead to a simpler definition for docs#pgame.has_le and docs#pgame.lf

[Violeta Hernández]

These are currently defined in terms of a single "mutual definition" docs#pgame.le_lf, which while effective, is certainly much more confusing

[Ruben Van de Velde]

I believe mutual inductive types are not that well supported in lean 3, so that might be more trouble than it's worth right now