def display_play.k

minebender-game@1.0.0.0 · proof_display.bend:298

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

298def display_play.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
299  +playing: {G.status(g) == T.Playing{} : T.Status}, +p: T.Pos, on: {L.on_board(w, h, p) == True{} : Bool},
300  c: PW.Canon(w, h, layout, g)) ->
301  {L.tile(g, p) == L.tile_of(L.seen(G.knowledge(g), p), G.flagged(g, p)) : T.Tile}:
302  match c:
303    case (eg, facts):
304      +s = PW.shown_of(g)
305      +f = PW.flags_of(g)
306      %Equal.sym(G.Game, g, G.Game{w, h, layout, s, f, G.status(g)}, eg) :
307        {L.tile(_, p) == L.tile_of(L.seen(G.knowledge(_), p), G.flagged(_, p)) : T.Tile}
308      %Equal.sym(T.Status, G.status(g), T.Playing{}, playing) :
309        {L.tile(G.Game{w, h, layout, s, f, _}, p)
310          == L.tile_of(L.seen(G.knowledge(G.Game{w, h, layout, s, f, _}), p), G.flagged(G.Game{w, h, layout, s, f, _}, p)) : T.Tile}
311      display_play_c(w, h, layout, s, f, p, on_conv(w, h, p, on))