An implementation of Tic-Tac-Toe in Agda

agda-tic-tac-toe is a formalization of the rules of tic-tac-toe.

Here's what an example game looks like:

example : Game
example = cross (move 1F 1F) $
          naught (move 0F 0F) $
          cross (move 0F 1F) $
          naught (move 1F 0F) $
          cross (move 2F 1F) $
          game-over

Note that all game validity conditions (IE: not being able to play in the same place twice, play must end after someone wins) are all automated using tactic arguments.

Also included are some helpful macros for displaying the current board state, which looks something like this:

display-example : Game
display-example =
  cross (move 1F 1F) $
  naught (move 0F 0F) $
  cross (move 0F 1F) $
  display-board

/Users/reedmullanix/Documents/Projects/agda-tic-tac-toe/src/Games/TicTacToe.agda:239,5-10
Board:

O | X |  
---------
  | X |  
---------
  |   |  

when checking that the expression unquote display-board has type
Moves O (play (move 0F 1F))