From 14095d29f98cdf6fe4a7ac97e63c66b81d1ea93f Mon Sep 17 00:00:00 2001 From: dianne Date: Fri, 28 Dec 2018 02:42:32 -0800 Subject: [PATCH] fix an error in the definition of adjacency --- Minesweeper/Coords.agda | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Minesweeper/Coords.agda b/Minesweeper/Coords.agda index c971fb3..3ef6a40 100644 --- 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