This repository contains a correct-by-construction implementation of the card solitaire game FreeCell that's guaranteed to allow any valid move and disallow any invalid move.
The rules are standard FreeCell - the goal is to move all of the cards to the foundations. The piles (cells/foundations/cascades) are labeled from 0 to f; enter a source pile label followed by a space and then a destination pile label (e.g. 5 e) to move a card from one pile to another. Enter win to check if you've won, and quit to quit.
agda --compile Main.agda. Building requires the Agda standard library to be installed and associated with the name standard-libarary in an Agda defaults file.