law loop_some

minebender-game@1.0.0.0 · proof_solver.bend:2271

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/solver.bend as S

2271# When the loop names c, c is one of its cells and its search found nothing.
2272law loop_some:
2273  for +hs: List<&2, T.Pos>
2274  for +found: List<&2, T.Grid(Bool)>
2275  for +todo: S.Plan
2276  for +part: T.Grid(Maybe<&2, Bool>)
2277  for +ctx: S.Ctx
2278  for +c: T.Pos
2279  for e: {S.loop(hs, found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>}
2280  LoopSome(hs, todo, part, ctx, c)