SetTheory.Game.Pgame

Stream: mathlib4

[Maxwell Thum]

At https://github.com/leanprover-community/mathlib4/blob/port/SetTheory.Game.Pgame/Mathlib/SetTheory/Game/Pgame.lean#L217 I get the error

code generator does not support recursor 'Pgame.recOn' yet, consider using 'match ... with' and/or structural recursion

I don't know how to go about using either.

[Eric Wieser]

x.recOn fun yl yr yL yR => IH (mk yl yr yL yR) should be something like match x with mk yl yr yL yR => IH (mk yl yr yL yR) end

[Maxwell Thum]

match x with | mk yl yr yL yR => IH (mk yl yr yL yR) gives me a type mismatch for IH (mk yl yr yL yR)