def start_cover.seen

minebender-game@1.0.0.0 · proof_solver.bend:2114

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

2114def start_cover.seen(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +its: List<&2, S.Item>, +q: T.Pos,
2115  on: {B.on_board(w, h, q) == True{} : Bool}, +s: T.Seen, se: {B.at(T.Seen, T.Hidden{}, rows, q) == s : T.Seen}) ->
2116  {Bool.or(Bool.not(S.is_none(S.start.cell(s))), tcontains(S.order(S.todos(its, S.hidden_cells(rows, B.cells(w, h)))), q))
2117    == True{} : Bool}:
2118  match s:
2119    case T.Hidden{}:
2120      +hs = S.hidden_cells(rows, B.cells(w, h))
2121      order_member(S.todos(its, hs), q,
2122        %Equal.sym(Bool, tcontains(S.todos(its, hs), q), B.contains(hs, q), tcontains_todos(its, hs, q)) : {_ == True{} : Bool};
2123        hc_member(rows, B.cells(w, h), q, PS.cells_member(w, h, q, on),
2124          %Equal.sym(T.Seen, B.at(T.Seen, T.Hidden{}, rows, q), T.Hidden{}, se) : {S.is_hidden(_) == True{} : Bool}; {==}))
2125    case T.Shown{k}:
2126      {==}
2127    case T.Boom{}:
2128      {==}