def touching_member.go

minebender-game@1.0.0.0 · proof_cells.bend:431

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/proof_grid.bend as PG

431def touching_member.go(+s: T.Pos, +e0: T.Pos, +t: List<&2, T.Pos>, +r: T.Pos,
432  a: {B.adjacent(s, r) == True{} : Bool}, +b: Bool, be: {B.same(e0, r) == b : Bool},
433  m: {Bool.or(b, B.contains(t, r)) == True{} : Bool},
434  ih: {B.contains(t, r) == True{} : Bool} -> {B.contains(B.touching(s, t), r) == True{} : Bool}) ->
435  {B.contains(List.filter.put(T.Pos, e0, B.touching(s, t), B.adjacent(s, e0)), r) == True{} : Bool}:
436  match b:
437    case True{}:
438      %Equal.sym(T.Pos, e0, r, PG.same_sound(e0, r, be)) :
439        {B.contains(List.filter.put(T.Pos, _, B.touching(s, t), B.adjacent(s, _)), r) == True{} : Bool}
440      %Equal.sym(Bool, B.adjacent(s, r), True{}, a) :
441        {B.contains(List.filter.put(T.Pos, r, B.touching(s, t), _), r) == True{} : Bool}
442      PG.contains_cons_self(r, B.touching(s, t))
443    case False{}:
444      put_keeps(e0, B.touching(s, t), B.adjacent(s, e0), r, ih(m))