minebender-game

Releases (1)

• 1.0.0.0 indexed

Definitions (1,011)

proof_laws.bend

• def open_mono.go
• law open_mono
• def reveal_mono.go
• law reveal_mono
• law chord_mono
• def flag_mono.go
• def assist_mono.safe
• def assist_mono.pick
• def assist_mono.go
• law step_mono
• law inv_of
• def vis_partsA revealed cell of the knowledge is on the board and revealed in the game.
• def monotone.k2
• def monotone.k
• def monotone.r
• law monotone_
• def mine_on.col
• def mine_on.row
• law mine_onA mine of a w-by-h layout is on the board.
• law path_closedIn a closed grid, a zero walk from a revealed cell ends at a revealed cell.
• def unrev_true
• def is_lost_wop
• def start_ok
• def start_has
• law open_mine_c
• def open_safe_c.go
• law open_safe_c
• def flood_complete_c.go
• law flood_complete_c
• def exact_explode
• def flood_exact_c.go
• law flood_exact_c
• def open_mine.k
• law open_mine_
• def open_safe.k
• law open_safe_
• def flood_complete.k
• law flood_complete_
• def flood_exact.k
• law flood_exact_

proof_lists.bend

• def Maybe.disc_n
• def none_ne_some
• def Maybe.val
• def some_inj
• law set_len
• law get_set_eq
• law get_set_ne
• law set_outSetting an index past the end changes nothing.
• law get_inInside a list, an index reads Some of its default.
• law rows_wide_getA row of a grid whose rows all have w cells has w cells.
• def row_of
• law shaped_len
• law shaped_wide
• law row_inIn a w-by-h grid, the row at y < h is its row and has w cells.
• law at_set_eq
• law row_in_get
• law row_in_len
• def at_set_ne.row
• def at_set_ne.go
• law at_set_neSetting p leaves every other cell as it was.
• law rows_wide_set
• law shaped_set
• law rep_len
• law rep_wide
• law blank_shaped
• law rep_default
• law blank_at
• law row_false_set
• law count_false_set.go
• law count_false_setRevealing an unrevealed cell of the board uses up one count.
• law count_false_zeroA grid with no unrevealed cell has every cell of the board revealed.
• def count_false_zero.go

proof_solver.bend

• def one
• def tf
• def nf
• law row_mines_sum
• law total_sum
• law count_sum
• law row_true_sum
• law row_none_sum
• law part_true_sum
• law part_none_sum
• law true_among_sum
• law none_among_sum
• def beq
• law beq_sound
• law beq_refl
• def cmp_cell
• type CE
• def cmp_f.go
• def cmp_f
• def completesThe layout has every cell the partial layout fixes.
• law comp_cell
• law cell_lo
• law cell_hi
• law among_lo
• law among_hi
• def item_onb
• def items_onbEvery revealed cell of the items, and every cell its number counts, is on the board.
• def sum_eq_cells