Minesweeper.Reasoning is an Agda module providing a formal description of the game Minesweeper and proofs about it, inspired by ProofSweeper. In ProofSweeper, you play Minesweeper by formally proving in Idris that cells are or aren't mines, using some provided axioms, rather than simply clicking to uncover them. My goal with Minesweeper.Reasoning is to prove that those axioms are sound (if you use them to prove that a cell is or isn't a mine, that will always be the case) and complete (if a cell is always or never a mine, you can prove it with those axioms).
These proofs are found in Minesweeper/Reasoning.agda. The formalization of Minesweeper is split across the remaining modules;
of note, Minesweeper/Rules.agda and Minesweeper/Moves.agda contain the main definitions, along with some useful lemmas.
Minesweeper.Reasoning was checked against Agda v2.6.0.1 and requires agda-stdlib v1.1.