fix an error in the definition of adjacency

dianne · Dec 28, 2018 · 14095d2 · 14095d2
1 parent cfe6ea6
commit 14095d2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda
@@ -16,10 +16,10 @@ Coords : Bounds → Set
 Coords (w , h) = Fin w × Fin h
 
 Adjacent : ∀ {bounds} (coords₁ coords₂ : Coords bounds) → Set
-Adjacent (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ x₂ ⊖ toℕ x₂ ∣ ≡ 1
+Adjacent (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ≡ 1
 
 adjacent? : ∀ {bounds} → Decidable (Adjacent {bounds})
-adjacent? (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ x₂ ⊖ toℕ x₂ ∣ ≟ 1
+adjacent? (x₁ , y₁) (x₂ , y₂) = ∣ toℕ x₁ ⊖ toℕ x₂ ∣ ⊔ ∣ toℕ y₁ ⊖ toℕ y₂ ∣ ≟ 1
 
 Neighbor : ∀ {bounds} (coords : Coords bounds) → Set
 Neighbor coords = Σ[ neighbor ∈ _ ] Adjacent coords neighbor