Minesweeper.idr

module Minesweeper

-- row, col
Point : Type
Point = (Nat, Nat)

-- rows, cols, mines (should be a set; should be constrained to rows/columns)
Board : Type
Board = (Nat, Nat, List Point)

-- mine?, mine neighbor count
Cell : Type
Cell = (Bool, Nat)

-- rows of cells, columns of cells (should be vectors of specific length)
Projection : Type
Projection = List (List Cell)

-- record a mine and update its neighbors
addMine : Projection -> Point -> Projection

-- create an empty projection of the given dimensions
emptyProjection : Nat -> Nat -> Projection

-- project the board
projectBoard : Board -> Projection