def at_set_mono.go

minebender-game@1.0.0.0 · proof_flood.bend:62

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

62def at_set_mono.go(+g: T.Grid(Bool), +p: T.Pos, +q: T.Pos, e: {B.at(Bool, False{}, g, q) == True{} : Bool},
63  +b: Bool, be: {B.same(p, q) == b : Bool}) ->
64  {B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q) == True{} : Bool}:
65  match b:
66    case True{}:
67      %Equal.sym(T.Pos, p, q, PG.same_sound(p, q, be)) :
68        {B.at(Bool, False{}, B.set_at(Bool, g, _, True{}), q) == True{} : Bool}
69      at_true_self(g, q, e)
70    case False{}:
71      %Equal.sym(Bool, B.at(Bool, False{}, B.set_at(Bool, g, p, True{}), q), B.at(Bool, False{}, g, q),
72        PL.at_set_ne(Bool, g, p, q, True{}, False{}, be)) : {_ == True{} : Bool}
73      e