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-overNote 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))
React
Typescript
Django
Laravel
Facebook
Microsoft
Google
Alibaba
D3
Tencent