def covered_extract.go

minebender-game@1.0.0.0 · proof_solver.bend:2190

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

2190def covered_extract.go(+ctx: S.Ctx, +l: T.Grid(Bool), +t: List<&2, T.Grid(Bool)>, +c: T.Pos,
2191  +vl: {S.check(ctx, l) == True{} : Bool},
2192  r: Or({B.mine(l, c) == True{} : Bool}, {S.covered(t, c) == True{} : Bool}),
2193  ih: {S.covered(t, c) == True{} : Bool} -> Witness(ctx, c)) -> Witness(ctx, c):
2194  match r:
2195    case Inl{m}:
2196      (l, (vl, m))
2197    case Inr{cv}:
2198      ih(cv)