diff --git a/Board.agda b/Minesweeper/Board.agda similarity index 91% rename from Board.agda rename to Minesweeper/Board.agda index 18bdd8a..02fa982 100644 --- a/Board.agda +++ b/Minesweeper/Board.agda @@ -1,8 +1,10 @@ +module Minesweeper.Board where + open import Data.Vec as Vec using (Vec) open import Data.Product open import Relation.Binary.PropositionalEquality -open import Coords +open import Minesweeper.Coords Board : Set → Bounds → Set Board A (w , h) = Vec (Vec A w) h diff --git a/Coords.agda b/Minesweeper/Coords.agda similarity index 91% rename from Coords.agda rename to Minesweeper/Coords.agda index d9f3d65..c971fb3 100644 --- a/Coords.agda +++ b/Minesweeper/Coords.agda @@ -1,3 +1,5 @@ +module Minesweeper.Coords where + open import Data.Nat open import Data.Integer using (∣_∣; _⊖_) open import Data.Product @@ -5,7 +7,7 @@ open import Data.Fin hiding (_≟_) open import Relation.Binary using (Decidable) open import Relation.Binary.PropositionalEquality -open import Enumeration as Enum using (Enumeration) +open import Minesweeper.Enumeration as Enum using (Enumeration) Bounds : Set Bounds = ℕ × ℕ diff --git a/Enumeration.agda b/Minesweeper/Enumeration.agda similarity index 99% rename from Enumeration.agda rename to Minesweeper/Enumeration.agda index 241ec5f..d8e5f4e 100644 --- a/Enumeration.agda +++ b/Minesweeper/Enumeration.agda @@ -1,4 +1,4 @@ -module Enumeration where +module Minesweeper.Enumeration where open import Data.List as List using (List; []; _∷_) import Data.List.Categorical as List diff --git a/Moves.agda b/Minesweeper/Moves.agda similarity index 93% rename from Moves.agda rename to Minesweeper/Moves.agda index 4331c53..a9f7b6a 100644 --- a/Moves.agda +++ b/Minesweeper/Moves.agda @@ -1,8 +1,10 @@ -- a hopefully-self-evident description of valid minesweeper moves -open import Coords -open import Board -open import Rules +module Minesweeper.Moves where + +open import Minesweeper.Coords +open import Minesweeper.Board +open import Minesweeper.Rules data Tile : Set where known : KnownTile → Tile diff --git a/Rules.agda b/Minesweeper/Rules.agda similarity index 93% rename from Rules.agda rename to Minesweeper/Rules.agda index d15b178..539c1f3 100644 --- a/Rules.agda +++ b/Minesweeper/Rules.agda @@ -1,5 +1,7 @@ -- the rules of filled minesweeper boards: do the numbers tell the truth? +module Minesweeper.Rules where + open import Data.Unit open import Data.Product open import Data.Nat as ℕ using (ℕ) @@ -9,9 +11,9 @@ open import Relation.Binary using () renaming (Decidable to Decidable₂) open import Relation.Unary using () renaming (Decidable to Decidable₁) open import Relation.Nullary -open import Coords -open import Board -open import Enumeration as Enum using (Enumeration) +open import Minesweeper.Coords +open import Minesweeper.Board +open import Minesweeper.Enumeration as Enum using (Enumeration) data KnownTile : Set where mine : KnownTile