PROOF.flag_others.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/PROOF.bend as PROOF
Lines 274-287 of minebender-game@1.0.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/PROOF.bend&start_line=274&end_line=287

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

def flag_others.go(+c: Bool, +g: G.Game, +p: T.Pos, +q: T.Pos,
  d: {B.same(p, q) == False{} : Bool}) ->
  {G.flagged(G.flag.go(c, g, p), q) == G.flagged(g, q) : Bool}:
  match c:
    case False{}:
      {==}
    case True{}:
      match g:
        case G.Game{w, h, layout, shown, flags, status}:
          %Equal.sym(Bool, B.contains(G.toggle(flags, p), q), B.contains(flags, q),
            PG.toggle_other(flags, p, q, d)) :
            {Bool.and(G.unrevealed(w, h, shown, q), _)
              == Bool.and(G.unrevealed(w, h, shown, q), B.contains(flags, q)) : Bool}
          {==}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=contains
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=same
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=Game
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=flag.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=flagged
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=toggle
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=unrevealed
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_grid.bend&name=toggle_other
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos