def set_keep

minebender-game@1.0.0.0 · proof_solver.bend:1171

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_base.bend as P
import minebender-game@1.0.0.0/proof_grid.bend as PG
import minebender-game@1.0.0.0/proof_lists.bend as PL

1171def set_keep(+part: T.Grid(Maybe<&2, Bool>), +c: T.Pos, +q: T.Pos, +v: Maybe<&2, Bool>, +bq: Bool,
1172  fre: {S.is_none(S.look(part, c)) == True{} : Bool}, lq: {S.look(part, q) == Some{bq} : Maybe<&2, Bool>},
1173  +b: Bool, be: {B.same(c, q) == b : Bool}) ->
1174  {S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q) == Some{bq} : Maybe<&2, Bool>}:
1175  match b:
1176    case True{}:
1177      +lc = {%Equal.sym(T.Pos, c, q, PG.same_sound(c, q, be)) : {S.look(part, _) == Some{bq} : Maybe<&2, Bool>};
1178        lq : {S.look(part, c) == Some{bq} : Maybe<&2, Bool>}}
1179      Empty.absurd({S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q) == Some{bq} : Maybe<&2, Bool>},
1180        P.false_ne_true(%lc : {S.is_none(_) == True{} : Bool}; fre))
1181    case False{}:
1182      %Equal.sym(Maybe<&2, Bool>, S.look(B.set_at(Maybe<&2, Bool>, part, c, v), q), S.look(part, q),
1183        PL.at_set_ne(Maybe<&2, Bool>, part, c, q, v, None{}, be)) : {_ == Some{bq} : Maybe<&2, Bool>}
1184      lq