Misere combinatorial games.

class MisereGames.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 MisereGames.«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 MisereGames.«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 MisereGames.ofSetsTactic : Lean.ParserDescr

Discharge validity side conditions generated by the !{...} notation.

Equations

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

def MisereGames.«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 MisereGames.«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 MisereGames.delabOfSets : Lean.PrettyPrinter.Delaborator.Delab

Delaborator for the !{st} and !{s | t} notation.

Equations

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

theorem MisereGames.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}