a couple high-level comments

Enumeration.agda

@@ -25,6 +25,12 @@ open import Data.Sum as Sum
 open import Category.Monad
 import Level
 
+-- in order to talk about the number of mines adjacent to a tile, we define Enumeration:
+-- a list of all the elements of a type, with each appearing once.
+-- our goal here is to develop the necessary machinery to do that. specifically, we need
+-- that all Enumerations of a type have the same length (they're unique up to bag equality),
+-- and we need to be able to be able to enumerate the adjacent mines of a tile, (which we
+-- get by enumerating any m×n grid and filtering by a predicate)
 record Enumeration A : Set where
   field
     list : List A

Moves.agda

@@ -12,18 +12,21 @@ data Guess : Set where
   mine⚐ : Guess
   safe⚐ : Guess
 
+-- tile filling: an unknown tile can be filled with anything
 data _↝▣_ : Tile → KnownTile → Set where
   ↝▣known   : ∀ s → known s ↝▣ s
   ↝▣unknown : ∀ s → unknown ↝▣ s
 
+-- board filling: can a fully filled board be reached by filling in the unknown tiles of a partial board?
 _↝⊞_ : ∀ {bounds} → Board Tile bounds → Board KnownTile bounds → Set
 holey ↝⊞ filled = ∀ coords → lookup coords holey ↝▣ lookup coords filled
 
+-- guessing: is a guess of a tile's type valid for that tile?
 data _↝⚐_ : Guess → KnownTile → Set where
   ↝⚐mine : mine⚐ ↝⚐ mine
   ↝⚐safe : ∀ n → safe⚐ ↝⚐ safe n
 
--- move validity relation: a guess is valid when it holds in every rule-respecting way to fill the board's unfilled tiles
+-- move validity: a guess as to a tile's identity on a board is valid when it holds in every rule-respecting way to fill the board's unfilled tiles
 _[_]↝✓_ : ∀ {bounds} → Board Tile bounds → Coords bounds → Guess → Set
 grid [ coords ]↝✓ guess = ∀ grid′ →
   grid ↝⊞ grid′ →

Rules.agda

@@ -17,14 +17,18 @@ data KnownTile : Set where
   mine : KnownTile
   safe : ℕ → KnownTile
 
+-- a numbered tile is good if the number on it matches the number of mines adjacent to it.
+-- since all Enumerations of a type have the same length, it's sufficient to provide only one as evidence
 _[_]✓ : ∀ {bounds} → Board KnownTile bounds → Coords bounds → Set
 _[_]✓ {bounds} grid coords with lookup coords grid
 ... | mine = ⊤
 ... | safe n = Σ[ neighboringMines ∈ Enumeration (mine Neighboring coords on grid) ] n ≡ length (Enumeration.list neighboringMines)
 
+-- a board is good if all positions on it are good
 _✓ : ∀ {bounds} → Board KnownTile bounds → Set
 _✓ {bounds} grid = ∀ coords → grid [ coords ]✓
 
+
 mine? : Decidable₁ (_≡_ mine)
 mine? mine     = yes refl
 mine? (safe _) = no  λ { () }