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.
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.
- out : x.ShortAux
Instances
theorem
IGame.Short.mk'
{x : IGame}
(h₁ : x.leftMoves.Finite)
(h₂ : x.rightMoves.Finite)
(h₃ : ∀ y ∈ x.leftMoves, y.Short)
(h₄ : ∀ y ∈ x.rightMoves, y.Short)
:
x.Short
Alias of IGame.Short.isOption
.
@[irreducible]
Alias of IGame.Short.subposition
.