Surreal Games make "non valid occurrence"

Stream: lean4

[Op From The Start]

I am trying to formalize myself the surreal numbers. I have come to a problem that the type system does not know that the system is well founded.

unsafe
inductive Game (γ: Ordinal)
 /-
 (kernel) arg #6 of 'Game.mk' contains a non valid occurrence of the datatypes being declared
 -/
 | mk (LS RS: Type u) (α β : Ordinal)
    (l: LS → Game α ) (r: RS → Game β )
    (hα: α < γ) (hβ: β < γ)

def is_ge{α β : Ordinal}(x: Game α)(y: Game β) : Prop := by
have xc: Game α := x
have yc: Game β := y
cases x with
| mk _ xRS _ xO _ xR _ _ =>
cases y with
| mk yLS _ yO _ yL _ _ _ =>
exact (∀ xr: xRS,¬ is_ge yc (xR xr)) ∧ (∀ yl: yLS,¬ is_ge (yL yl) xc)
termination_by (α × β)

unsafe
instance zero : Game 1 := Game.mk PEmpty PEmpty 0 0
(fun (x:PEmpty) => x.elim) (fun (x:PEmpty) => x.elim)
(by rw [← Ordinal.succ_zero]; exact Ordinal.succ_pos 0)
(by rw [← Ordinal.succ_zero]; exact Ordinal.succ_pos 0)

unsafe
instance one : Game 2 := Game.mk (Game 1) PEmpty 1 0
(fun (_:Game 1) => zero )
(fun (x:PEmpty) => x.elim)
(by rw [← Ordinal.succ_one]; exact Order.lt_succ 1)
(by rw [← Ordinal.succ_one]; exact Ordinal.succ_pos 1)

What can I do to fix this?

[Edward van de Meent]

You might be interested in looking how mathlib does this, i.e. look at docs#SetTheory.PGame . My guess as to why your code doesn't work would be that it has to do with the type depending on ordinals?

[Edward van de Meent]

my guess as to what specifically is going on is that you can't vary the parameter of an inductive declaration, i.e. when defining Game a, you can't refer to Game b