def tput_self

minebender-game@1.0.0.0 · proof_solver.bend:1927

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
import minebender-game@1.0.0.0/proof_base.bend as P

1927def tput_self(+b: Bool, +c: T.Pos, +rel: List<&2, S.Item>, +rest: List<&2, S.Todo>, +q: T.Pos,
1928  bt: {b == True{} : Bool}, cq: {B.same(c, q) == True{} : Bool}) ->
1929  {tcontains(List.filter.put(S.Todo, S.Todo{c, rel}, rest, b), q) == True{} : Bool}:
1930  match b:
1931    case True{}:
1932      %Equal.sym(Bool, B.same(c, q), True{}, cq) : {Bool.or(_, tcontains(rest, q)) == True{} : Bool}
1933      {==}
1934    case False{}:
1935      Empty.absurd({tcontains(rest, q) == True{} : Bool}, P.false_ne_true(bt))