law dfs_some_check

minebender-game@1.0.0.0 · proof_solver.bend:1120

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

1120# A layout the search returns passes the consistency check.
1121law dfs_some_check:
1122  for +todo: List<&2, S.Todo>
1123  for +part: T.Grid(Maybe<&2, Bool>)
1124  for +ctx: S.Ctx
1125  for +l: T.Grid(Bool)
1126  for e: {S.dfs(todo, part, ctx) == Some{l} : Maybe<&2, T.Grid(Bool)>}
1127  {S.check(ctx, l) == True{} : Bool}