ProofSolver.item_ok_agree: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 610-624 of minebender-game@1.0.0.0/proof_solver.bend: https://jend.leeeet.dev/read.txt?path=minebender-game@1.0.0.0/proof_solver.bend&start_line=610&end_line=624

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/solver.bend as S
import minebender-game@1.0.0.0/proof_cells.bend as PS

def item_ok_agree(+w: Nat, +h: Nat, +l1: T.Grid(Bool), +l2: T.Grid(Bool), +ag: {agree(w, h, l1, l2) == True{} : Bool},
  +p: T.Pos, +s: T.Seen, +ns: List<&2, T.Pos>, on: {B.on_board(w, h, p) == True{} : Bool},
  ons: {PS.allp(~PS.WH, ~PS.onb, PS.WH{w, h}, ns) == True{} : Bool}) ->
  {S.item_ok(s, p, ns, l1) == S.item_ok(s, p, ns, l2) : Bool}:
  match s:
    case T.Hidden{}:
      {==}
    case T.Shown{k}:
      %Equal.sym(Bool, B.mine(l1, p), B.mine(l2, p), agree_cell(w, h, l1, l2, ag, p, on)) :
        {Bool.and(Bool.not(_), Nat.is_eq(B.count_mines(l1, ns), k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
      %Equal.sym(Nat, B.count_mines(l1, ns), B.count_mines(l2, ns), count_agree(w, h, l1, l2, ag, ns, ons)) :
        {Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(_, k)) == Bool.and(Bool.not(B.mine(l2, p)), Nat.is_eq(B.count_mines(l2, ns), k)) : Bool}
      {==}
    case T.Boom{}:
      agree_cell(w, h, l1, l2, ag, p, on)

Uses (20):
  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.not
  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=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/board.bend&name=count_mines
  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=on_board
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=WH
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=allp
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_cells.bend&name=onb
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=agree
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=agree_cell
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=count_agree
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=item_ok
  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
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen