class OfSets (α : Type (u + 1)) (Valid : outParam ((Player → Set α) → Prop)) : Type (u + 1)

Type class for the ofSets operation. Used to implement the !{st} and !{s | t} syntax.

• ofSets (st : Player → Set α) (h : Valid st) [Small.{u, u + 1} ↑(st Player.left)] [Small.{u, u + 1} ↑(st Player.right)] : α

  Construct a combinatorial game from its Left and Right option sets.

  Conventions for notations in identifiers:

  • The recommended spelling of !{st}'h in identifiers is ofSets.

  • The recommended spelling of !{s | t}'h in identifiers is ofSets.

  • The recommended spelling of !{st} in identifiers is ofSets.

  • The recommended spelling of !{s | t} in identifiers is ofSets.

def «term!{_}'_» : Lean.ParserDescr

Construct a combinatorial game from its Left and Right option sets.

Conventions for notations in identifiers:

• The recommended spelling of !{st}'h in identifiers is ofSets.

Equations

• One or more equations did not get rendered due to their size.

def «term!{_|_}'_» : Lean.ParserDescr

Construct a combinatorial game from its Left and Right option sets.

Conventions for notations in identifiers:

• The recommended spelling of !{s | t}'h in identifiers is ofSets.

Equations

• One or more equations did not get rendered due to their size.

def tacticOf_sets_tactic : Lean.ParserDescr

Equations

• tacticOf_sets_tactic = Lean.ParserDescr.node `tacticOf_sets_tactic 1024 (Lean.ParserDescr.nonReservedSymbol "of_sets_tactic" false)

def «term!{_}» : Lean.ParserDescr

Construct a combinatorial game from its Left and Right option sets.

Conventions for notations in identifiers:

• The recommended spelling of !{st} in identifiers is ofSets.

Equations

• One or more equations did not get rendered due to their size.

def «term!{_|_}» : Lean.ParserDescr

Construct a combinatorial game from its Left and Right option sets.

Conventions for notations in identifiers:

• The recommended spelling of !{s | t} in identifiers is ofSets.

Equations

• One or more equations did not get rendered due to their size.

def delabOfSets : Lean.PrettyPrinter.Delaborator.Delab

Equations

• One or more equations did not get rendered due to their size.

theorem ofSets_eq_ofSets_cases {α : Type (u_1 + 1)} {Valid : (Player → Set α) → Prop} [OfSets α Valid] (st : Player → Set α) (h : Valid st) [Small.{u_1, u_1 + 1} ↑(st Player.left)] [Small.{u_1, u_1 + 1} ↑(st Player.right)] : !{st} = !{st Player.left | st Player.right}