namespacing: move modules to Minesweeper

dianne · Aug 20, 2018 · c557dc0 · c557dc0
1 parent 80f67e2
commit c557dc0
Show file tree

Hide file tree

Showing 5 changed files with 17 additions and 9 deletions.
diff --git a/Board.agda → Minesweeper/Board.agda b/Board.agda → 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 → Minesweeper/Coords.agda b/Coords.agda → Minesweeper/Coords.agda
@@ -1,11 +1,13 @@
+module Minesweeper.Coords where
+
 open import Data.Nat
 open import Data.Integer using (∣_∣; _⊖_)
 open import Data.Product
 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 → Minesweeper/Enumeration.agda b/Enumeration.agda → 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 → Minesweeper/Moves.agda b/Moves.agda → 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 → Minesweeper/Rules.agda b/Rules.agda → 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