def consistent

minebender-game@1.0.0.0 · LAWS.bend:166

import Base
import minebender-game@1.0.0.0/types.bend as T

166# The layout could be the real one, given everything the player sees: it has
167# the board's shape, exactly the announced number of mines, a mine under
168# every Boom, none under a number, and every number counts its neighbours.
169def consistent(v: T.Knowledge, +layout: T.Grid(Bool)) -> Bool:
170  match v:
171    case T.Knowledge{+w, +h, n, +rows}:
172      shaped(Bool, w, h, layout) && shaped(T.Seen, w, h, rows)
173        && Nat.is_eq(total_mines(layout), n)
174        && agrees_all(w, h, rows, layout, cells(w, h))