MSGSS
The hard way: making inductive data types via initial algebras in Lean4
Sometimes Lean can be finicky. Maybe you try to define a well-founded type, but Lean does not except it. In this talk I will describe my experience trying to define games in Lean via the quotient of a polynomial functor and its fixed point. We will also go over how to manually define a fold.