Skip to content

Commit

Permalink
remove some unused definitions
Browse files Browse the repository at this point in the history
I added them at the very start when I wasn't quite sure what I wanted or needed;
at this point they're just not necessary anywhere.
  • Loading branch information
dianne committed Feb 25, 2019
1 parent 82c7701 commit d7c9d3f
Showing 1 changed file with 0 additions and 12 deletions.
12 changes: 0 additions & 12 deletions Minesweeper/Moves.agda
Original file line number Diff line number Diff line change
Expand Up @@ -52,18 +52,6 @@ grid [ coords ]↝✓ guess = ∀ grid′ →
grid′ ✓
guess ⚐✓ lookup coords grid′

-- solvable boards: a board is solvable when there is a rule-respecting way to fill its unfilled tiles
record Solvable {bounds} (unsolved : Board Tile bounds) : Set where
field
solution : Board KnownTile bounds
relevance : unsolved ↝⊞ solution
validity : solution ✓

-- "play" a valid move on a solvable board, giving evidence that it holds in the provided solution
play : {bounds grid} (coords : Coords bounds) {guess}
grid [ coords ]↝✓ guess (solved : Solvable grid)
guess ⚐✓ lookup coords (Solvable.solution solved)
play coords move solved = move (Solvable.solution solved) (Solvable.relevance solved) (Solvable.validity solved)


invert⚐ : Guess Guess
Expand Down

0 comments on commit d7c9d3f

Please sign in to comment.