def loop_some.cov

minebender-game@1.0.0.0 · proof_solver.bend:2257

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

2257def loop_some.cov(+c0: T.Pos, +t: List<&2, T.Pos>, +found: List<&2, T.Grid(Bool)>, +todo: S.Plan,
2258  +part: T.Grid(Maybe<&2, Bool>), +ctx: S.Ctx, +c: T.Pos, +b: Bool,
2259  e: {S.loop.if(b, u => S.loop(t, found, todo, part, ctx),
2260      v => S.loop.found(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx))) == Some{c} : Maybe<&2, T.Pos>},
2261  ihf: {S.loop(t, found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c),
2262  ihn: @l: T.Grid(Bool) -> {S.loop(t, l <> found, todo, part, ctx) == Some{c} : Maybe<&2, T.Pos>} -> LoopSome(t, todo, part, ctx, c)) ->
2263  LoopSome(c0 <> t, todo, part, ctx, c):
2264  match b:
2265    case True{}:
2266      loop_some.lift(c0, t, todo, part, ctx, c, ihf(e))
2267    case False{}:
2268      loop_some.found(c0, t, found, todo, part, ctx, c,
2269        loop_found_some(S.search(c0, todo, part, ctx), c0, l => S.loop(t, l <> found, todo, part, ctx), c, e), ihn)