ProofInv.all_safe_set_mine.go: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_inv.bend as ProofInv
Lines 507-522 of minebender-game@1.0.0.0/proof_inv.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_inv.bend&start_line=507&end_line=522

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

def all_safe_set_mine.go(+layout: T.Grid(Bool), +shown: T.Grid(Bool), +p: T.Pos,
  +mp: {B.mine(layout, p) == True{} : Bool}, ps: List<&2, T.Pos>) ->
  {G.all_safe.go(layout, B.set_at(Bool, shown, p, True{}), ps) == G.all_safe.go(layout, shown, ps) : Bool}:
  match ps:
    case Nil{}:
      {==}
    case +q <> t:
      +s2 = B.set_at(Bool, shown, p, True{})
      %Equal.sym(Bool, G.all_safe.go(layout, s2, t), G.all_safe.go(layout, shown, t),
        all_safe_set_mine.go(layout, shown, p, mp, t)) :
        {Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, s2, q)), _)
          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
      %all_safe_cell(layout, shown, p, q, mp, B.same(p, q), {==}) :
        {Bool.and(_, G.all_safe.go(layout, shown, t))
          == Bool.and(Bool.or(B.mine(layout, q), B.at(Bool, False{}, shown, q)), G.all_safe.go(layout, shown, t)) : Bool}
      {==}

Uses (13):
  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=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=mine
  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/board.bend&name=set_at
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/game.bend&name=all_safe.go
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_inv.bend&name=all_safe_cell
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Grid
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Pos