minebender-game
Releases (1)
-
1.0.0.0 indexed
Definitions (1,011)
game.bend
- def tile_shown
- def tile.go
- def tile_at
- def disp_row
- def disp_rows
- def display
- def flags_shownHow many flags the mine counter shows: the mines, less the flags placed.
proof_assist.bend
- def not_and_false
- def SafeAt
- def first_safe.lift
- def first_safe.go2
- law first_safe_someWhile some safe cell is unrevealed, first_safe finds one.
- law all_safe_append
- law on_drop
- law on_take
- def on_turn
- def on_put
- law on_edges
- def on_listEvery cell the assist may look at is on the board.
- def nos_listWhile a safe cell is hidden, the assist's list holds one.
- def stuck_pick.none
- def stuck_pick
- def assist_stuck.k
- law assist_stuck_
- def early_pick
- def assist_early.k
- law assist_too_early_
proof_base.bend
- def Bool.disc_ft
- law false_ne_true
- law true_ne_false
- law and_true_l
- law and_true_r
- law not_not
- def Nat.disc_z
- law succ_ne_zero
- law eq_refl
- law lt_irrefl
- law eq_sound
- law lt_zero
- law sub_zero
- law add_one
- law add_zero
- law add_succ
- def lt_succ.zero
- def lt_succ.lift
- law lt_succi < 1+p means i < p or i = p.
- law append_nil
- law append_assoc
- law length_append
- law get_append_lBefore index length(xs), xs ++ ys reads like xs.
- law get_append_len
- law range_acc
- law range_snoc
- law range_length
- law range_get
- def range_get.cases
- law and_false_r
- law or_false_l
- law get_outPast its end, a list has nothing.
- law range_get_out
- law add_comm
- law add_assoc
- law add_left_comm
- law mul_zero_r
- law mul_succ_r
- law mul_comm
- law le_zero
- law le_zero_l
- law le_nea <= b and a != b give a + 1 <= b.
- law lt_succ_len < k + 1 gives n <= k.
- law or_false_inv
- law and_true_r_id
- law not_true
- law not_false
- law succ_inj
- def pred
- law le_of_add
- def LeW
- def le_witness.lift
- law le_witness
- law add_swap
- def le_add.k
- law le_add
- law le_refl
- law or_false_r
proof_cells.bend
- def allpEvery cell of ps passes f (with e for f's context).
- def allp_head
- def allp_tail
- def allp_member.go
- def allp_memberA cell of a list whose cells all pass f passes f.
- def contains_append.or
- law contains_append
- def memnA Nat list contains i.
- def or_true_r
- law memn_append_r
- law memn_append_l
- def memn_append_l.go
- def memn_range.cases
- law memn_range
- def contains_row.go