def bridge.k

minebender-game@1.0.0.0 · proof_laws.bend:260

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

260def bridge.k(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +g: G.Game,
261  shape: {L.shaped(Bool, w, h, layout) == True{} : Bool}, c: Canon(w, h, layout, g)) ->
262  {L.consistent(G.knowledge(g), layout) == True{} : Bool}:
263  match c:
264    case (eg, facts):
265      %Equal.sym(G.Game, g, G.Game{w, h, layout, shown_of(g), flags_of(g), G.status(g)}, eg) :
266        {L.consistent(G.knowledge(_), layout) == True{} : Bool}
267      bridge_canon(w, h, layout, shown_of(g), flags_of(g), G.status(g), shape)