ProofSolver.start_comp.cell: def of minebender-game@1.0.0.0
Import: import minebender-game@1.0.0.0/proof_solver.bend as ProofSolver
Lines 1550-1566 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=1550&end_line=1566

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/LAWS.bend as L
import minebender-game@1.0.0.0/proof_base.bend as P
import minebender-game@1.0.0.0/proof_copy.bend as PC

def start_comp.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos, +s: T.Seen,
  ag: {L.agrees(w, h, layout, q, s) == True{} : Bool}) ->
  {cmp_cell(S.start.cell(s), B.mine(layout, q)) == True{} : Bool}:
  match s:
    case T.Hidden{}:
      {==}
    case T.Shown{k}:
      %Equal.sym(Bool, B.mine(layout, q), False{}, P.not_true(B.mine(layout, q),
        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {Bool.not(_) == True{} : Bool};
        P.and_true_l(Bool.not(L.mine(layout, q)), Nat.is_eq(L.adj_mines(w, h, layout, q), k), ag))) :
        {beq(_, False{}) == True{} : Bool}
      {==}
    case T.Boom{}:
      %Equal.sym(Bool, B.mine(layout, q), True{},
        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {_ == True{} : Bool}; ag) :
        {beq(_, True{}) == True{} : Bool}
      {==}

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=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/LAWS.bend&name=adj_mines
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=agrees
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/LAWS.bend&name=mine
  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/proof_base.bend&name=and_true_l
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_base.bend&name=not_true
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_copy.bend&name=mine_eq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=beq
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/proof_solver.bend&name=cmp_cell
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/solver.bend&name=start.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
  https://jend.leeeet.dev/definition.txt?path=minebender-game@1.0.0.0/types.bend&name=Seen