From d7c9d3fece050f71ff6f0472e0c39fd34db623ca Mon Sep 17 00:00:00 2001 From: dianne Date: Sun, 24 Feb 2019 23:17:54 -0800 Subject: [PATCH] remove some unused definitions 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. --- Minesweeper/Moves.agda | 12 ------------ 1 file changed, 12 deletions(-) diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda index bdde15b..0f4790e 100644 --- a/Minesweeper/Moves.agda +++ b/Minesweeper/Moves.agda @@ -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