Documentation

CombinatorialGames.Game.Short

Short games #

A combinatorial game is Short if it has only finitely many subpositions. In particular, this means there is a finite set of moves at every point.

We historically defined Short x as data, which we then used to enable some degree of computation on combinatorial games. This functionality is now implemented through the game_cmp tactic instead.

@[irreducible]
Equations
Instances For
    class IGame.Short (x : IGame) :

    A short game is one with finitely many subpositions. That is, the left and right sets are finite, and all of the games in them are short as well.

    Instances
      theorem IGame.Short.mk' {x : IGame} (h₁ : x.leftMoves.Finite) (h₂ : x.rightMoves.Finite) (h₃ : yx.leftMoves, y.Short) (h₄ : yx.rightMoves, y.Short) :
      theorem IGame.Short.of_mem_leftMoves {x y : IGame} [h : x.Short] (hy : y x.leftMoves) :
      theorem IGame.Short.of_mem_rightMoves {x y : IGame} [h : x.Short] (hy : y x.rightMoves) :
      theorem IGame.Short.isOption {x y : IGame} [x.Short] (h : y.IsOption x) :
      theorem IGame.IsOption.short {x y : IGame} [x.Short] (h : y.IsOption x) :

      Alias of IGame.Short.isOption.

      @[irreducible]
      theorem IGame.Short.subposition {y x : IGame} [x.Short] (h : y.Subposition x) :
      @[simp]
      @[simp]
      @[irreducible]
      instance IGame.Short.neg (x : IGame) [x.Short] :
      (-x).Short
      @[simp]
      @[irreducible]
      instance IGame.Short.add (x y : IGame) [x.Short] [y.Short] :
      (x + y).Short
      instance IGame.Short.sub (x y : IGame) [x.Short] [y.Short] :
      (x - y).Short
      instance IGame.Short.natCast (n : ) :
      (↑n).Short
      instance IGame.Short.intCast (n : ) :
      (↑n).Short
      @[irreducible]
      instance IGame.Short.mul (x y : IGame) [x.Short] [y.Short] :
      (x * y).Short
      instance IGame.Short.mulOption (x y a b : IGame) [x.Short] [y.Short] [a.Short] [b.Short] :
      (mulOption x y a b).Short