Theory of impartial combinatorial games in Coq. This includes:
- Definition of an impartial game and a sum of games.
- Equivalence of games.
- Equivalence of sum of Nim games to a single Nim game.
- Grundy numbers and Sprague-Grundy theorem.
Run make
.
This also builds clickable HTML pages, courtesy of CoqDocJS.