def flag_others.go

minebender-game@1.0.0.0 · PROOF.bend:274

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/proof_grid.bend as PG

274def flag_others.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos,
275  d: {B.same(p, q) == False{} : Bool}) ->
276  {G.flagged(G.flag.go(c, g, p), q) == G.flagged(g, q) : Bool}:
277  match c:
278    case False{}:
279      {==}
280    case True{}:
281      match g:
282        case G.Game{w, h, layout, shown, flags, status}:
283          %Equal.sym(Bool, B.contains(G.toggle(flags, p), q), B.contains(flags, q),
284            PG.toggle_other(flags, p, q, d)) :
285            {Bool.and(G.unrevealed(w, h, shown, q), _)
286              == Bool.and(G.unrevealed(w, h, shown, q), B.contains(flags, q)) : Bool}
287          {==}