minebender-game

Releases (1):
  1.0.0.0  0x581b7b5abb55b3363cb439c0fb72d761  indexed  https://jend.leeeet.dev/files.txt?path=minebender-game@1.0.0.0

Definitions (1011, 1 to 100 shown):
  LAWS.at (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=at)
   # The value of grid g at p, or d when p is off the grid.
   def at(-A: Data, d: A, g: T.Grid(A), p: T.Pos) -> A:
  LAWS.mine (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine)
   def mine(layout: T.Grid(Bool), p: T.Pos) -> Bool:
  LAWS.on_board (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=on_board)
   def on_board(w: Nat, h: Nat, p: T.Pos) -> Bool:
  LAWS.same (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=same)
   def same(p: T.Pos, q: T.Pos) -> Bool:
  LAWS.dist (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=dist)
   def dist(+a: Nat, +b: Nat) -> Nat:
  LAWS.within_one (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=within_one)
   # p and q are at most one step apart in each direction (or the same cell).
   def within_one(p: T.Pos, q: T.Pos) -> Bool:
  LAWS.adjacent (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=adjacent)
   # p and q are two different cells that touch, by a side or a corner.
   def adjacent(+p: T.Pos, +q: T.Pos) -> Bool:
  LAWS.row_cells (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=row_cells)
   # The cells of row y, from column 0 up.
   def row_cells(+y: Nat, xs: List<&2, Nat>) -> List<&2, T.Pos>:
  LAWS.cells.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=cells.go)
   def cells.go(+w: Nat, ys: List<&2, Nat>) -> List<&2, T.Pos>:
  LAWS.cells (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=cells)
   # Every cell of a w-by-h board, row by row.
   def cells(w: Nat, h: Nat) -> List<&2, T.Pos>:
  LAWS.touching (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=touching)
   # The cells of qs adjacent to p, in the order of qs.
   def touching(+p: T.Pos, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
  LAWS.neighbours (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=neighbours)
   # The cells of the board adjacent to p, row by row.
   def neighbours(w: Nat, h: Nat, p: T.Pos) -> List<&2, T.Pos>:
  LAWS.count_mines (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=count_mines)
   def count_mines(+layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> Nat:
  LAWS.adj_mines (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=adj_mines)
   # The number a revealed safe cell p must show.
   def adj_mines(w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> Nat:
  LAWS.row_mines (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=row_mines)
   def row_mines(row: List<&2, Bool>) -> Nat:
  LAWS.total_mines (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=total_mines)
   def total_mines(layout: T.Grid(Bool)) -> Nat:
  LAWS.rows_wide (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=rows_wide)
   def rows_wide(-A: Data, +w: Nat, g: T.Grid(A)) -> Bool:
  LAWS.shaped (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=shaped)
   # g has exactly h rows of exactly w cells.
   def shaped(-A: Data, w: Nat, h: Nat, +g: T.Grid(A)) -> Bool:
  LAWS.seen (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=seen)
   def seen(v: T.Knowledge, p: T.Pos) -> T.Seen:
  LAWS.is_hidden (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_hidden)
   def is_hidden(s: T.Seen) -> Bool:
  LAWS.hidden (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=hidden)
   # p is a cell of the board that the player cannot see.
   def hidden(v: T.Knowledge, +p: T.Pos) -> Bool:
  LAWS.revealed (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=revealed)
   # p is a cell of the board that the player can see.
   def revealed(v: T.Knowledge, +p: T.Pos) -> Bool:
  LAWS.agrees (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees)
   # What the player sees at p agrees with the layout.
   def agrees(w: Nat, h: Nat, +layout: T.Grid(Bool), +p: T.Pos, s: T.Seen) -> Bool:
  LAWS.agrees_all (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees_all)
   def agrees_all(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool),
     ps: List<&2, T.Pos>) -> Bool:
  LAWS.consistent (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=consistent)
   # The layout could be the real one, given everything the player sees: it has
   # the board's shape, exactly the announced number of mines, a mine under
   # every Boom, none under a number, and every number counts its neighbours.
   def consistent(v: T.Knowledge, +layout: T.Grid(Bool)) -> Bool:
  LAWS.ProvablySafe (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=ProvablySafe)
   # p is hidden, and no layout consistent with what the player knows has a mine on p.
   def ProvablySafe(v: T.Knowledge, p: T.Pos) -> Type:
  LAWS.Stuck (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=Stuck)
   # No cell is provably safe: the player's only options are guesses.
   def Stuck(v: T.Knowledge) -> Type:
  LAWS.all_safe_revealed.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=all_safe_revealed.go)
   # Every safe cell of the board is revealed.
   def all_safe_revealed.go(+v: T.Knowledge, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> Bool:
  LAWS.all_safe_revealed (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=all_safe_revealed)
   def all_safe_revealed(+v: T.Knowledge, layout: T.Grid(Bool)) -> Bool:
  LAWS.zero (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=zero)
   # A zero: a safe cell of the board with no adjacent mine.
   def zero(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos) -> Bool:
  LAWS.zero_walk (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=zero_walk)
   # Starting at p, the path steps from cell to adjacent cell of the board,
   # leaving only zeros, and ends at q. The empty path goes from p to p.
   def zero_walk(path: List<&2, T.Pos>, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
     +p: T.Pos, q: T.Pos) -> Bool:
  LAWS.is_won (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_won)
   def is_won(s: T.Status) -> Bool:
  LAWS.is_lost (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_lost)
   def is_lost(s: T.Status) -> Bool:
  LAWS.play (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=play)
   # Take the actions in order.
   def play(acts: List<&2, T.Action>, g: G.Game) -> G.Game:
  LAWS.Reachable (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=Reachable)
   # The game g arises from a fresh game on this layout by some actions.
   def Reachable(w: Nat, h: Nat, layout: T.Grid(Bool), g: G.Game) -> Type:
  LAWS.reveals (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=reveals)
   def reveals(ps: List<&2, T.Pos>) -> List<&2, T.Action>:
  LAWS.flags_among (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flags_among)
   # How many cells of qs are flagged.
   def flags_among(+g: G.Game, qs: List<&2, T.Pos>) -> Nat:
  LAWS.hidden_unflagged (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=hidden_unflagged)
   def hidden_unflagged(+g: G.Game, +v: T.Knowledge, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
  LAWS.chord_targets.pick (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord_targets.pick)
   def chord_targets.pick(+g: G.Game, v: T.Knowledge, +ns: List<&2, T.Pos>, s: T.Seen) ->
     List<&2, T.Pos>:
  LAWS.chord_targets.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord_targets.go)
   def chord_targets.go(g: G.Game, +v: T.Knowledge, +p: T.Pos) -> List<&2, T.Pos>:
  LAWS.chord_targets (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord_targets)
   # Chording on p: if p shows a number k and exactly k of its neighbours are
   # flagged, the hidden unflagged neighbours of p, row by row; otherwise none.
   def chord_targets(+g: G.Game, p: T.Pos) -> List<&2, T.Pos>:
  LAWS.bridge (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=bridge)
   # LAW: "The real board is always consistent with what the player sees."
   # Without it, the knowledge laws below would say nothing about the real game.
   # It also covers "every number equals its count of adjacent mines".
   law bridge:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     {consistent(G.knowledge(g), layout) == True{} : Bool}
  LAWS.won_iff (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=won_iff)
   # LAW: "The game is won exactly when every safe cell is revealed."
   law won_iff:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     {is_won(G.status(g)) == all_safe_revealed(G.knowledge(g), layout) : Bool}
  LAWS.monotone (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=monotone)
   # LAW: "A revealed cell stays revealed, showing the same thing."
   # With bridge, this makes every action that changes the knowledge reveal at least
   # one more cell, so a game has at most w*h such actions.
   law monotone:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for a: T.Action
     …
  LAWS.frozen (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=frozen)
   # LAW: "Once the game is won or lost, no action changes anything."
   law frozen:
     for g: G.Game
     for over: {G.status(g) != T.Playing{} : T.Status}
     for a: T.Action
     {G.step(g, a) == g : G.Game}
  LAWS.open_mine (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=open_mine)
   # LAW: "Revealing a mine loses, naming that mine, and shows it as Boom."
   law open_mine:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for p: T.Pos
     for boom: {mine(layout, p) == True{} : Bool}
     …
  LAWS.open_safe (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=open_safe)
   # LAW: "Revealing a safe cell never loses."
   law open_safe:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for p: T.Pos
     for safe: {mine(layout, p) == False{} : Bool}
     {is_lost(G.status(G.open(g, p))) == False{} : Bool}
  LAWS.flood_complete (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flood_complete)
   # LAW: "Revealing a cell p reveals every cell reached from p by a path
   # through zeros" (so a 0 opens its whole 0-region and the numbers around it;
   # for a mine, that is p alone).
   law flood_complete:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     …
  LAWS.flood_exact (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flood_exact)
   # LAW: "Revealing p reveals nothing else": every newly revealed cell is
   # reached from p by a path through zeros. (For a mine, that is p alone.)
   law flood_exact:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for p: T.Pos
     …
  LAWS.reveal_flagged (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=reveal_flagged)
   # LAW: "Clicking a flagged cell does nothing."
   law reveal_flagged:
     for g: G.Game
     for p: T.Pos
     for flag: {G.flagged(g, p) == True{} : Bool}
     {G.step(g, T.Reveal{p}) == g : G.Game}
  LAWS.reveal_unflagged (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=reveal_unflagged)
   # LAW: "Clicking an unflagged cell reveals it."
   law reveal_unflagged:
     for g: G.Game
     for p: T.Pos
     for flag: {G.flagged(g, p) == False{} : Bool}
     {G.step(g, T.Reveal{p}) == G.open(g, p) : G.Game}
  LAWS.chord (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=chord)
   # LAW: "Double-clicking a number reveals its hidden unflagged neighbours,
   # one by one, row by row" (when exactly that many neighbours are flagged).
   law chord:
     for g: G.Game
     for p: T.Pos
     {G.step(g, T.Chord{p}) == play(reveals(chord_targets(g, p)), g) : G.Game}
  LAWS.flag_no_knowledge (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flag_no_knowledge)
   # LAW: "Flags are not knowledge": flagging changes neither what the player
   # sees nor the game's status.
   law flag_no_knowledge:
     for g: G.Game
     for p: T.Pos
     {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
     {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}
  LAWS.flag_toggle (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flag_toggle)
   # LAW: "Flagging a hidden cell during play toggles its flag."
   law flag_toggle:
     for g: G.Game
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for p: T.Pos
     for hid: {hidden(G.knowledge(g), p) == True{} : Bool}
     {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}
  LAWS.flag_others (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flag_others)
   # LAW: "Flagging p leaves every other cell's flag alone."
   law flag_others:
     for g: G.Game
     for p: T.Pos
     for q: T.Pos
     for diff: {p != q : T.Pos}
     {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}
  LAWS.flags_hidden (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flags_hidden)
   # LAW: "Only hidden cells carry flags": revealing a flagged cell clears its
   # flag, and no cell off the board is ever flagged.
   law flags_hidden:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for q: T.Pos
     for flag: {G.flagged(g, q) == True{} : Bool}
     {hidden(G.knowledge(g), q) == True{} : Bool}
  LAWS.flag_revealed (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=flag_revealed)
   # LAW: "Flagging a cell that is not hidden does nothing."
   law flag_revealed:
     for g: G.Game
     for p: T.Pos
     for vis: {hidden(G.knowledge(g), p) == False{} : Bool}
     {G.step(g, T.Flag{p}) == g : G.Game}
  LAWS.assist_stuck (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=assist_stuck)
   # LAW: "Pressing the assist when stuck reveals a safe cell."
   law assist_stuck:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for stuck: Stuck(G.knowledge(g))
     for k: Nat
     …
  LAWS.assist_too_early (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=assist_too_early)
   # LAW: "Pressing the assist when some cell is provably safe loses, and shows
   # a provably safe cell; the knowledge is unchanged."
   law assist_too_early:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for q: T.Pos
     …
  LAWS.clamp (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=clamp)
   def clamp(lo: Nat, hi: Nat, x: Nat) -> Nat:
  LAWS.custom (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=custom)
   # Windows XP's Custom Field dialog: width is clamped to 9..30, height to
   # 9..25 and mines to 10..999, then mines are capped at width*height - 10.
   def custom(w: Nat, h: Nat, m: Nat) -> T.Setup:
  LAWS.level_beginner (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=level_beginner)
   # LAW: "Beginner is 9 by 9 with 10 mines."
   law level_beginner:
     {G.setup(T.Beginner{}) == T.Setup{9n, 9n, 10n} : T.Setup}
  LAWS.level_intermediate (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=level_intermediate)
   # LAW: "Intermediate is 16 by 16 with 40 mines."
   law level_intermediate:
     {G.setup(T.Intermediate{}) == T.Setup{16n, 16n, 40n} : T.Setup}
  LAWS.level_expert (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=level_expert)
   # LAW: "Expert is 30 wide by 16 high with 99 mines."
   law level_expert:
     {G.setup(T.Expert{}) == T.Setup{30n, 16n, 99n} : T.Setup}
  LAWS.level_custom (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=level_custom)
   # LAW: "A custom level is limited exactly as Windows XP limits it."
   law level_custom:
     for w: Nat
     for h: Nat
     for m: Nat
     {G.setup(T.Custom{w, h, m}) == custom(w, h, m) : T.Setup}
  LAWS.gen_shape (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=gen_shape)
   # LAW: "Generated boards have the requested shape."
   law gen_shape:
     for w: Nat
     for h: Nat
     for n: Nat
     for first: T.Pos
     for rs: List<&2, U32>
     {shaped(Bool, w, h, G.place_mines(w, h, n, first, rs)) == True{} : Bool}
  LAWS.gen_count (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=gen_count)
   # LAW: "Generated boards have exactly n mines" (when they fit beside the first
   # click).
   law gen_count:
     for w: Nat
     for h: Nat
     for n: Nat
     for first: T.Pos
     for rs: List<&2, U32>
     for on: {on_board(w, h, first) == True{} : Bool}
     for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
     {total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}
  LAWS.gen_first_safe (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=gen_first_safe)
   # LAW: "The first click is safe."
   law gen_first_safe:
     for w: Nat
     for h: Nat
     for n: Nat
     for first: T.Pos
     for rs: List<&2, U32>
     {mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}
  LAWS.gen_opening (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=gen_opening)
   # LAW: "When there's room, the first click opens an area: no mine on it or
   # next to it." (As in Windows Vista and later.)
   law gen_opening:
     for w: Nat
     for h: Nat
     for n: Nat
     for first: T.Pos
     for rs: List<&2, U32>
     for room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
     for q: T.Pos
     for near: {within_one(first, q) == True{} : Bool}
     {mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}
  LAWS.tile (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=tile)
   # What the screen shows at p.
   def tile(g: G.Game, p: T.Pos) -> T.Tile:
  LAWS.tile_of (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=tile_of)
   # How a cell looks given what the player sees there and their flag.
   def tile_of(s: T.Seen, flag: Bool) -> T.Tile:
  LAWS.is_covered (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_covered)
   def is_covered(t: T.Tile) -> Bool:
  LAWS.display_play (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=display_play)
   # LAW: "During play, the screen shows exactly what the player knows, and
   # their flags": nothing about the hidden mines leaks onto the screen.
   law display_play:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for playing: {G.status(g) == T.Playing{} : T.Status}
     for p: T.Pos
     …
  LAWS.display_blast (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=display_blast)
   # LAW: "After an explosion, the screen shows the mine that exploded."
   law display_blast:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for p: T.Pos
     for lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}
     for on: {on_board(w, h, p) == True{} : Bool}
     {tile(g, p) == T.Blast{} : T.Tile}
  LAWS.display_hint (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=display_hint)
   # LAW: "After the assist is pressed too early, the screen shows the safe cell
   # the player could have revealed."
   law display_hint:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for s: T.Pos
     for lost: {G.status(g) == T.Lost{T.AssistTooEarly{s}} : T.Status}
     …
  LAWS.display_mines (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=display_mines)
   # LAW: "Once the game is over, no mine stays covered."
   law display_mines:
     for w: Nat
     for h: Nat
     for layout: T.Grid(Bool)
     for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
     for g: G.Game
     for r: Reachable(w, h, layout, g)
     for over: {G.status(g) != T.Playing{} : T.Status}
     for q: T.Pos
     for on: {on_board(w, h, q) == True{} : Bool}
     …
  PROOF.Bool.disc (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=Bool.disc)
   def Bool.disc(b: Bool) -> Type:
  PROOF.Bool.false_ne_true (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=Bool.false_ne_true)
   def Bool.false_ne_true(e: {False{} == True{} : Bool}) -> Empty:
  PROOF.open_over (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=open_over)
   # In a finished game, opening a cell changes nothing.
   law open_over:
     for +g: G.Game
     for +p: T.Pos
     for +over: {G.is_playing(G.status(g)) == False{} : Bool}
     {G.open(g, p) == g : G.Game}
  PROOF.not_playing (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=not_playing)
   law not_playing:
     for +s: T.Status
     for ne: {s != T.Playing{} : T.Status}
     {G.is_playing(s) == False{} : Bool}
  PROOF.reveal_go_same (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=reveal_go_same)
   law reveal_go_same:
     for +b: Bool
     for +g: G.Game
     for +p: T.Pos
     for +e: {G.open(g, p) == g : G.Game}
     {G.reveal.go(b, g, p) == g : G.Game}
  PROOF.reveal_over (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=reveal_over)
   law reveal_over:
     for +g: G.Game
     for +p: T.Pos
     for +over: {G.is_playing(G.status(g)) == False{} : Bool}
     {G.reveal(g, p) == g : G.Game}
  PROOF.chord_over (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=chord_over)
   law chord_over:
     for +ts: List<&2, T.Pos>
     for +g: G.Game
     for +over: {G.is_playing(G.status(g)) == False{} : Bool}
     {G.chord_play(ts, g) == g : G.Game}
  PROOF.flag_over (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_over)
   law flag_over:
     for +g: G.Game
     for +p: T.Pos
     for +over: {G.is_playing(G.status(g)) == False{} : Bool}
     {G.flag(g, p) == g : G.Game}
  PROOF.assist_over (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=assist_over)
   law assist_over:
     for +g: G.Game
     for +over: {G.is_playing(G.status(g)) == False{} : Bool}
     for +k: Nat
     {G.assist(g, k) == g : G.Game}
  PROOF.frozen_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=frozen_)
   law frozen_:
     for +g: G.Game
     for over: {G.status(g) != T.Playing{} : T.Status}
     for a: T.Action
     {G.step(g, a) == g : G.Game}
  PROOF.reveal_flagged_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=reveal_flagged_)
   law reveal_flagged_:
     for +g: G.Game
     for +p: T.Pos
     for +flag: {G.flagged(g, p) == True{} : Bool}
     {G.step(g, T.Reveal{p}) == g : G.Game}
  PROOF.reveal_unflagged_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=reveal_unflagged_)
   law reveal_unflagged_:
     for +g: G.Game
     for +p: T.Pos
     for +flag: {G.flagged(g, p) == False{} : Bool}
     {G.step(g, T.Reveal{p}) == G.open(g, p) : G.Game}
  PROOF.flag_k.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_k.go)
   def flag_k.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
     {G.knowledge(G.flag.go(b, g, p)) == G.knowledge(g) : T.Knowledge}:
  PROOF.flag_s.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_s.go)
   def flag_s.go(+b: Bool, +g: G.Game, +p: T.Pos) ->
     {G.status(G.flag.go(b, g, p)) == G.status(g) : T.Status}:
  PROOF.flag_no_knowledge_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_no_knowledge_)
   law flag_no_knowledge_:
     for +g: G.Game
     for +p: T.Pos
     {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
     {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}
  PROOF.status_disc_playing (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=status_disc_playing)
   def status_disc_playing(s: T.Status) -> Type:
  PROOF.won_ne_playing (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=won_ne_playing)
   def won_ne_playing(e: {T.Won{} == T.Playing{} : T.Status}) -> Empty:
  PROOF.lost_ne_playing (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=lost_ne_playing)
   def lost_ne_playing(-why: T.Loss, e: {T.Lost{why} == T.Playing{} : T.Status}) -> Empty:
  PROOF.flag_toggle_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_toggle_)
   law flag_toggle_:
     for +g: G.Game
     for +playing: {G.status(g) == T.Playing{} : T.Status}
     for +p: T.Pos
     for +hid: {L.hidden(G.knowledge(g), p) == True{} : Bool}
     {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}
  PROOF.flag_others.go (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_others.go)
   def flag_others.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos,
     d: {B.same(p, q) == False{} : Bool}) ->
     {G.flagged(G.flag.go(c, g, p), q) == G.flagged(g, q) : Bool}:
  PROOF.flag_others_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_others_)
   law flag_others_:
     for +g: G.Game
     for +p: T.Pos
     for +q: T.Pos
     for diff: {p != q : T.Pos}
     {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}
  PROOF.flag_revealed_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=flag_revealed_)
   law flag_revealed_:
     for +g: G.Game
     for +p: T.Pos
     for +vis: {L.hidden(G.knowledge(g), p) == False{} : Bool}
     {G.step(g, T.Flag{p}) == g : G.Game}
  PROOF.play_reveals (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=play_reveals)
   law play_reveals:
     for +ts: List<&2, T.Pos>
     for +g: G.Game
     {G.chord_play(ts, g) == L.play(L.reveals(ts), g) : G.Game}
  PROOF.chord_ (https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/PROOF.bend&name=chord_)
   law chord_:
     for +g: G.Game
     for +p: T.Pos
     {G.step(g, T.Chord{p}) == L.play(L.reveals(L.chord_targets(g, p)), g) : G.Game}
More: https://jend.leeeet.dev/packages/minebender-game.txt?definitions_offset=100