minebender-game
Releases (1)
-
1.0.0.0 indexed
Definitions (1,011)
proof_cells.bend
- law contains_row
- def contains_cells.k
- def contains_cells.go
- law contains_cells
- law cells_memberEvery cell of the board is one of its cells.
- type WH
- def onb
- law allp_append
- def allnEvery element of xs is below n.
- law lt_mono
- law lt_succ_self
- law alln_mono
- law alln_append
- law alln_range
- law row_on
- law cells_on.go
- law cells_onEvery cell of cells(w, h) is on the board.
- law put_keeps
- def touching_member.go
- law touching_member
- law neighbours_memberAn adjacent cell of the board is a neighbour.
- type WHS
- def adj_on.go
- def adj_on
- def touching_all.go
- law touching_all
- law neighbours_allEvery neighbour of s is adjacent to s and on the board.
- law add_zero_l
- law add_zero_r
- law one_zero
- def count_zero_member.go
- law count_zero_memberA list with no mines has no mine on any of its cells.
- law zero_nbrThe neighbours of a zero have no mines.
proof_copy.bend
- law at_eq
- law mine_eq
- law on_board_eq
- law same_eq
- law adjacent_eq
- law row_cells_eq
- law cells_go_eq
- law cells_eq
- law touching_eq
- law neighbours_eq
- law count_mines_eq
- law adj_mines_eq
- law row_mines_eq
- law total_mines_eq
- law rows_wide_eq
- law shaped_eq
- law zero_eq
- law is_hidden_eq
- law seen_eq
- law hidden_eq
- law flags_among_eq
- law hidden_unflagged_eq
- law chord_pick_eq
- def chord_targets_eq.go
- law chord_targets_eq
proof_display.bend
- law disp_row_get
- law disp_rows_get
- law disp_atOn the board, the screen shows what tile_at says.
- law play_cell
- law display_play_c
- law display_blast_c
- law display_hint_c
- law over_cellA mine, once the game is over, under each way the cell might be marked.
- def mark_cell
- def mark_ok.pick
- def mark_ok.why
- law mark_okWhat the end of the game singles out is never covered.
- law display_mines_c
- def on_conv
- def display_play.k
- law display_play_
- def display_blast.k
- law display_blast_
- def display_hint.k
- law display_hint_
- def display_mines.k
- law display_mines_
proof_flood.bend
- def at_true_self.col
- def at_true_self.row
- law at_true_self
- def at_set_mono.go
- law at_set_monoRevealing a cell keeps every revealed cell revealed.
- law flood_shaped
- law flood_mono
- def wcontainsSome queued cell is q.
- def wcontains_append_r.go
- law wcontains_append_r
- def wcontains_append_l.go
- law wcontains_append_l
- def wcontains_works.go
- law wcontains_works
- law push_keeps
- law unrev_on
- law unrev_hidden
- law unrev_shown
- law count_after
- law at_set_on