Finished proof of solution for tic-tac-toe, but also noticed that in the formulation, the cases where there is one spot left (and thus only X moves) results in a false hypothesis.

Proved 4 of 9 cases for when X starts in 00

Found a pattern for part of the proof, but repeat isn't working

Last helper is defined, now we need some proof tactics maybe

successfully formalized safe (I think). Added more functions so that it is possible to detect invalid states during the proof

Addingttt

Merging in fabian's changes

Some cleanup

Intelligent player tree decision tree generation appears to be working ... so slow

Intelligent player is semi-working, where evaluate_moves is merely a stub (same behavior as naive player actually), now the hard part

Got something working, but probably buggy

Some cleanup and making players modular.

Created proofs file, proved that naive_player vs naive_player results in second player victory

Made playGameWithPlayers return an outcome instead of game (for easy proofs), but kept the old function as well for debugging purposes

Build now extracts correct function, and always extracts haskell