def loop_none.pick2

minebender-game@1.0.0.0 · proof_solver.bend:2339

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

2339def loop_none.pick2(+ctx: S.Ctx, +c0: T.Pos, +t: List<&2, T.Pos>, +c: T.Pos, +found: List<&2, T.Grid(Bool)>,
2340  mr: Or({B.same(c0, c) == True{} : Bool}, {B.contains(t, c) == True{} : Bool}),
2341  cov: {S.covered(found, c0) == True{} : Bool}, val: {all_valid(ctx, found) == True{} : Bool},
2342  k: {B.contains(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
2343  match mr:
2344    case Inl{cq}:
2345      witness_move(ctx, c0, c, cq, covered_extract(ctx, found, c0, cov, val))
2346    case Inr{mt}:
2347      k(mt)