ProofDisplay.display_mines.k: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_display.bend as ProofDisplay
Lines 386-398 of minebender-game@1.0.0.0/proof_display.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_display.bend&start_line=386&end_line=398

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L
import minebender-game@1.0.0.0/proof_copy.bend as PC
import minebender-game@1.0.0.0/proof_laws.bend as PW

def display_mines.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
  over: {G.status(g) != T.Playing{} : T.Status}, +q: T.Pos, on: {L.on_board(w, h, q) == True{} : Bool},
  m: {L.mine(layout, q) == True{} : Bool}, c: PW.Canon(w, h, layout, g)) ->
  {L.is_covered(L.tile(g, q)) == False{} : Bool}:
  match c:
    case (eg, facts):
      +s = PW.shown_of(g)
      +f = PW.flags_of(g)
      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
        {L.is_covered(L.tile(_, q)) == False{} : Bool}
      display_mines_c(w, h, layout, s, f, G.status(g), over, q, on_conv(w, h, q, on),
        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) :
          {_ == True{} : Bool}; m)

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=is_covered
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=tile
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=status
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_display.bend&name=display_mines_c
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_display.bend&name=on_conv
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=Canon
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=flags_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_laws.bend&name=shown_of
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Status