minebender-game

Releases (1)

• 1.0.0.0 indexed

Definitions (1,011)

proof_grid.bend

• def know_row_get.some
• law know_row_get
• law know_rows_get
• law know_atOn the board, the knowledge shows what seen_at says.
• law hidden_pick
• def know_hidden.go
• law know_hiddenHidden in the knowledge means on the board and not revealed in the game.
• law same_refl
• law same_sound
• def same_ne.go
• law same_ne
• law contains_cons_self
• def contains_remove_self.go
• law contains_remove_self
• def contains_remove_other.go
• law contains_remove_other
• def toggle_self.go
• law toggle_selfToggling p flips whether p is in the list.
• def toggle_other.go
• law toggle_otherToggling p leaves every other cell as it was.

proof_inv.bend

• def shown_in
• type CL
• def cl_f.go
• def cl_f
• def closed
• def closed_use.go
• law closed_useIn a closed grid, a revealed zero's neighbours are revealed.
• def flood_fact.goThe flood's one-cell closure fact: a revealed zero's neighbour is revealed.
• def closed_flood.nbrs
• def closed_flood.cell
• def closed_flood.cells
• law closed_floodA flood from a closed grid leaves a closed grid.
• def zero_not_mine
• def explode_fact.go
• def closed_explode.nbrs
• def closed_explode.cell
• def closed_explode.cells
• law closed_explode
• def closed_blank.cell
• def closed_blank.cells
• law closed_blank
• type LS
• def nsm_f.go
• def nsm_f
• def nsm
• def nsm_use.go
• law nsm_useWithout a revealed mine, a mine of the board is not revealed.
• def nsm_flood.walk
• def nsm_flood.new
• def nsm_flood.cell
• def nsm_flood.cells
• law nsm_floodA flood from a safe cell reveals no mine.
• def nsm_blank.cell
• def nsm_blank.cells
• law nsm_blank
• law won_or_playing_won
• law playing_is
• def calm
• def Facts
• def InvWhat every real game satisfies: the board it was started with, a grid of revealed cells of the board's shape, Won exactly when every safe cell is revealed, no revealed mine during play, and every revealed zero's neighbours revealed.
• def all_safe_cell
• def all_safe_set_mine.go
• law all_safe_set_mine
• def inv_open.go
• law inv_open
• def inv_reveal.go
• def inv_flag.go
• def inv_assist.safe
• def inv_assist.pick
• def inv_assist.go
• law inv_revealOver a game in its general form.
• law inv_flag
• law inv_assist
• law inv_chord
• law inv_step
• law inv_play
• law inv_fresh
• law inv_reachEvery real game satisfies the invariant.

proof_laws.bend

• def shown_of
• def flags_of
• def Canon
• law canonA real game in its canonical form, with the facts of the invariant.
• law know_seen
• law revealed_pick
• law know_revealedOn the board, revealed in the knowledge means revealed in the game.
• law know_row_len
• law know_rows_len
• law know_rows_wide
• law know_shaped
• def agrees_pick
• def agrees_cell
• def agrees_all_cells
• law bridge_canon
• def bridge.k
• law bridge_
• def safe_rev_cell
• def safe_rev_all
• def won_iff.k
• law won_iff_
• law flags_hidden_