def display_mines.k

minebender-game@1.0.0.0 · proof_display.bend:386

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

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