minebender-game

Releases (1)

• 1.0.0.0 indexed

Definitions (1,011)

LAWS.bend

• def atThe value of grid g at p, or d when p is off the grid.
• def mine
• def on_board
• def same
• def dist
• def within_onep and q are at most one step apart in each direction (or the same cell).
• def adjacentp and q are two different cells that touch, by a side or a corner.
• def row_cellsThe cells of row y, from column 0 up.
• def cells.go
• def cellsEvery cell of a w-by-h board, row by row.
• def touchingThe cells of qs adjacent to p, in the order of qs.
• def neighboursThe cells of the board adjacent to p, row by row.
• def count_mines
• def adj_minesThe number a revealed safe cell p must show.
• def row_mines
• def total_mines
• def rows_wide
• def shapedg has exactly h rows of exactly w cells.
• def seen
• def is_hidden
• def hiddenp is a cell of the board that the player cannot see.
• def revealedp is a cell of the board that the player can see.
• def agreesWhat the player sees at p agrees with the layout.
• def agrees_all
• def consistentThe layout could be the real one, given everything the player sees: it has the board's shape, exactly the announced number of mines, a mine under every Boom, none under a number, and every number counts its neighbours.
• def ProvablySafep is hidden, and no layout consistent with what the player knows has a mine on p.
• def StuckNo cell is provably safe: the player's only options are guesses.
• def all_safe_revealed.goEvery safe cell of the board is revealed.
• def all_safe_revealed
• def zeroA zero: a safe cell of the board with no adjacent mine.
• def zero_walkStarting at p, the path steps from cell to adjacent cell of the board, leaving only zeros, and ends at q.
• def is_won
• def is_lost
• def playTake the actions in order.
• def ReachableThe game g arises from a fresh game on this layout by some actions.
• def reveals
• def flags_amongHow many cells of qs are flagged.
• def hidden_unflagged
• def chord_targets.pick
• def chord_targets.go
• def chord_targetsChording on p: if p shows a number k and exactly k of its neighbours are flagged, the hidden unflagged neighbours of p, row by row; otherwise none.
• law bridgeLAW: "The real board is always consistent with what the player sees." Without it, the knowledge laws below would say nothing about the real game.
• law won_iffLAW: "The game is won exactly when every safe cell is revealed."
• law monotoneLAW: "A revealed cell stays revealed, showing the same thing." With bridge, this makes every action that changes the knowledge reveal at least one more cell, so a game has at most w*h such actions.
• law frozenLAW: "Once the game is won or lost, no action changes anything."
• law open_mineLAW: "Revealing a mine loses, naming that mine, and shows it as Boom."
• law open_safeLAW: "Revealing a safe cell never loses."
• law flood_completeLAW: "Revealing a cell p reveals every cell reached from p by a path through zeros" (so a 0 opens its whole 0-region and the numbers around it; for a mine, that is p alone).
• law flood_exactLAW: "Revealing p reveals nothing else": every newly revealed cell is reached from p by a path through zeros.
• law reveal_flaggedLAW: "Clicking a flagged cell does nothing."
• law reveal_unflaggedLAW: "Clicking an unflagged cell reveals it."
• law chordLAW: "Double-clicking a number reveals its hidden unflagged neighbours, one by one, row by row" (when exactly that many neighbours are flagged).
• law flag_no_knowledgeLAW: "Flags are not knowledge": flagging changes neither what the player sees nor the game's status.
• law flag_toggleLAW: "Flagging a hidden cell during play toggles its flag."
• law flag_othersLAW: "Flagging p leaves every other cell's flag alone."
• law flags_hiddenLAW: "Only hidden cells carry flags": revealing a flagged cell clears its flag, and no cell off the board is ever flagged.
• law flag_revealedLAW: "Flagging a cell that is not hidden does nothing."
• law assist_stuckLAW: "Pressing the assist when stuck reveals a safe cell."
• law assist_too_earlyLAW: "Pressing the assist when some cell is provably safe loses, and shows a provably safe cell; the knowledge is unchanged."
• def clamp
• def customWindows XP's Custom Field dialog: width is clamped to 9..30, height to 9..25 and mines to 10..999, then mines are capped at width*height - 10.
• law level_beginnerLAW: "Beginner is 9 by 9 with 10 mines."
• law level_intermediateLAW: "Intermediate is 16 by 16 with 40 mines."
• law level_expertLAW: "Expert is 30 wide by 16 high with 99 mines."
• law level_customLAW: "A custom level is limited exactly as Windows XP limits it."
• law gen_shapeLAW: "Generated boards have the requested shape."
• law gen_countLAW: "Generated boards have exactly n mines" (when they fit beside the first click).
• law gen_first_safeLAW: "The first click is safe."
• law gen_openingLAW: "When there's room, the first click opens an area: no mine on it or next to it." (As in Windows Vista and later.)
• def tileWhat the screen shows at p.
• def tile_ofHow a cell looks given what the player sees there and their flag.
• def is_covered
• law display_playLAW: "During play, the screen shows exactly what the player knows, and their flags": nothing about the hidden mines leaks onto the screen.
• law display_blastLAW: "After an explosion, the screen shows the mine that exploded."
• law display_hintLAW: "After the assist is pressed too early, the screen shows the safe cell the player could have revealed."
• law display_minesLAW: "Once the game is over, no mine stays covered."

PROOF.bend

• def Bool.disc
• def Bool.false_ne_true
• law open_overIn a finished game, opening a cell changes nothing.
• law not_playing
• law reveal_go_same
• law reveal_over
• law chord_over
• law flag_over
• law assist_over
• law frozen_
• law reveal_flagged_
• law reveal_unflagged_
• def flag_k.go
• def flag_s.go
• law flag_no_knowledge_
• def status_disc_playing
• def won_ne_playing
• def lost_ne_playing
• law flag_toggle_
• def flag_others.go
• law flag_others_
• law flag_revealed_
• law play_reveals
• law chord_