minebender-game
Search uses release 1.0.0.0 · 1,011 definitions
Definitions (1,011)
- law gen_row_len
- law gen_rows_len
- law gen_rows_wide
- def zoneThe zone a board of n mines keeps free around the first click.
- law gen_shape_
- def gen_bit_first
- law gen_row_firstA cell of a generated row that is in the zone has no mine.
- def Maybe.disc_some
- def gen_some_ne_none
- law gen_row_out
- law gen_rows_get
- law gen_rows_out
- def gen_first.col
- def gen_first.found
- def gen_first.row
- law sub_self
- law within_selfA cell is within one step of itself.
- law out_firstThe first click is always in its own zone.
- law gen_first_safe_
- law within_eq
- def opening_inA wide zone holds every cell next to the first click.
- law gen_opening_With room, no cell next to the first click gets a mine.
- def st_need
- def st_left
- def one
- def GenStepWhat one cell does to the state: the mines placed plus the mines still needed stay the same, need <= left stays true, and left counts down for every cell outside the zone.
- def gen_pick_false
- def gen_take
- def gen_cell.need
- def gen_cell.go
- law gen_cell
- def gen_row_count.step
- def gen_row_count.k2
- def gen_row_count.k
- law gen_row_count
- def gen_rows_count.k
- law gen_rows_count
- def outsHow many cells of ps are in the zone.
- def gen_left_firsts.go
- law gen_left_firstsEvery cell is either a candidate or in the zone.
- law firsts_append
- def cntHow many elements of xs are i.
- law cnt_append
- law cnt_step
- law cnt_rangeEach number below n appears in range(n) once.
- def firsts_row.end
- def firsts_row.go
- def firsts_rows.go
- law firsts_rows
- law row_cells_len
- law cells_go_len
- def one_when
- law le_trans
- def le_trans.k
- law add_cancel_l
- def swap3((a+b)+c) + ((a'+b')+c') regrouped as ((a+a')+(b+b')) + (c+c').
- def room_left.kRoom for n mines and 9 more among the L + O cells, with O <= 9: n <= L.
- def room_left
- def nrx is within one step of a.
- def ncntHow many elements of xs are within one step of a.
- def cnt1How many elements of xs are one below a.
- law near_ptWithin one step of a means a, a + 1 or a - 1.
- def near_pt.zx
- def near_pt.xz
- law near_cnt
- law cnt1_succ
- law cnt1_zero
- def pick_le1
- def cnt_le1
- def cnt1_le1
- law ncnt_le3At most three numbers below n are within one step of a.
- def wide_row.go
- def rsumEach row near the first click's row, counted c times.
- law wide_rows
- def pick_le3
- law rsum_le
- law wide_le9The zone around a first click holds at most 9 cells of the board.
- def cells_len
- law gen_inv_oneWith just the first click kept free, there are w*h - 1 candidates, so n < w*h mines fit among them.
- law gen_inv_wideWith room for 9 more, n mines fit outside the wider zone.
- def gen_inv.k
- law gen_invWhichever zone the board keeps free, the n mines fit outside it.
- law gen_count_