def loop_some.lift

minebender-game@1.0.0.0 · proof_solver.bend:2230

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

2230def loop_some.lift(+c0: T.Pos, +t: List<&2, T.Pos>, +todo: S.Plan, +part: T.Grid(Maybe<&2, Bool>),
2231  +ctx: S.Ctx, +c: T.Pos, r: LoopSome(t, todo, part, ctx, c)) -> LoopSome(c0 <> t, todo, part, ctx, c):
2232  match r:
2233    case (m, s):
2234      (or_r(B.same(c0, c), B.contains(t, c), m), s)