def start_comp.cell

minebender-game@1.0.0.0 · proof_solver.bend:1550

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

1550def start_comp.cell(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +q: T.Pos, +s: T.Seen,
1551  ag: {L.agrees(w, h, layout, q, s) == True{} : Bool}) ->
1552  {cmp_cell(S.start.cell(s), B.mine(layout, q)) == True{} : Bool}:
1553  match s:
1554    case T.Hidden{}:
1555      {==}
1556    case T.Shown{k}:
1557      %Equal.sym(Bool, B.mine(layout, q), False{}, P.not_true(B.mine(layout, q),
1558        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {Bool.not(_) == True{} : Bool};
1559        P.and_true_l(Bool.not(L.mine(layout, q)), Nat.is_eq(L.adj_mines(w, h, layout, q), k), ag))) :
1560        {beq(_, False{}) == True{} : Bool}
1561      {==}
1562    case T.Boom{}:
1563      %Equal.sym(Bool, B.mine(layout, q), True{},
1564        %Equal.sym(Bool, B.mine(layout, q), L.mine(layout, q), PC.mine_eq(layout, q)) : {_ == True{} : Bool}; ag) :
1565        {beq(_, True{}) == True{} : Bool}
1566      {==}