def tok_put

minebender-game@1.0.0.0 · proof_solver.bend:1762

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

1762def tok_put(+b: Bool, +t: S.Todo, +rest: List<&2, S.Todo>, +layout: T.Grid(Bool),
1763  ht: {todos_ok([t], layout) == True{} : Bool}, hr: {todos_ok(rest, layout) == True{} : Bool}) ->
1764  {todos_ok(List.filter.put(S.Todo, t, rest, b), layout) == True{} : Bool}:
1765  match b:
1766    case False{}:
1767      hr
1768    case True{}:
1769      match t:
1770        case S.Todo{c, rel}:
1771          %Equal.sym(Bool, todos_ok(rest, layout), True{}, hr) : {Bool.and(S.items_ok(rel, layout), _) == True{} : Bool}
1772          ht