def display_blast.k

minebender-game@1.0.0.0 · proof_display.bend:328

import Base
import minebender-game@1.0.0.0/types.bend as T
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_laws.bend as PW

328def display_blast.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game, +p: T.Pos,
329  +lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}, on: {L.on_board(w, h, p) == True{} : Bool},
330  c: PW.Canon(w, h, layout, g)) ->
331  {L.tile(g, p) == T.Blast{} : T.Tile}:
332  match c:
333    case (eg, facts):
334      +s = PW.shown_of(g)
335      +f = PW.flags_of(g)
336      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
337        {L.tile(_, p) == T.Blast{} : T.Tile}
338      %Equal.sym(T.Status, G.status(g), T.Lost{T.Exploded{p}}, lost) :
339        {L.tile(G.Game{w, h, layout, s, f, _}, p) == T.Blast{} : T.Tile}
340      display_blast_c(w, h, layout, s, f, p, on_conv(w, h, p, on))