Inductive types containing sets of them selfs

Stream: Is there code for X?

[Conando]

I am really new to lean but one of the thinks that sparked my interested was to force my self to really understand and complete the proofs in the book about combinatorial game theory. The issue though arises right at the beginning with how to start. At it's core it's an inductive type that has one constructor that takes a pair of Sets of this type. But next to all of my ideas face the issue of "[the constructor] has a non positive occurrence of the datatypes being declared". And I was unable to split this type into a family of types parameterized by the naturals. And advice, hints or ideas are appreciated.

[Adam Topaz]

You may want to look through the following file from mathlib to get some inspiration: https://github.com/leanprover-community/mathlib4/blob/5a4b605e9b5b793a0ea1fa648acd5400d3c4bf95/Mathlib/SetTheory/Game/PGame.lean

[Conando]

Oh thank you