Misere combinatorial games.

class MisereGames.Ruleset (R : Type u) : Type (u + 1)

A playable ruleset whose positions map to GameForms.

• toGameForm : R → GameForm

  The game form represented by a ruleset position.

• moves_toGameForm (p : Player) (r : R) (g' : GameForm) : g' ∈ Moves.moves p (toGameForm r) → ∃ (r' : R), toGameForm r' = g'

def MisereGames.Ruleset.Forms (R : Type u) [Ruleset R] (g : GameForm) : Prop

Set of GameForms created by the positions in ruleset R.

Equations

• MisereGames.Ruleset.Forms R g = ∃ (r : R), g = MisereGames.Ruleset.toGameForm r

theorem MisereGames.Ruleset.Forms.exists {R : Type u} [Ruleset R] {g : GameForm} (h_g : Forms R g) : ∃ (r : R), g = toGameForm r

theorem MisereGames.Ruleset.Forms.position_mem {R : Type u} [Ruleset R] (r : R) : Forms R (toGameForm r)

instance MisereGames.instHereditaryGameFormForms {R : Type u} [Ruleset R] : Form.Hereditary (Ruleset.Forms R)