def leaf_cell.go

minebender-game@1.0.0.0 · proof_solver.bend:863

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

863def leaf_cell.go(+part: T.Grid(Maybe<&2, Bool>), +layout: T.Grid(Bool), +q: T.Pos, +m: Maybe<&2, Bool>,
864  me: {S.look(part, q) == m : Maybe<&2, Bool>},
865  cv: {Bool.not(S.is_none(m)) == True{} : Bool}, cm: {cmp_cell(m, B.mine(layout, q)) == True{} : Bool}) ->
866  {beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}:
867  match m:
868    case None{}:
869      Empty.absurd({beq(B.mine(S.fill(part), q), B.mine(layout, q)) == True{} : Bool}, P.false_ne_true(cv))
870    case Some{c}:
871      %Equal.sym(Bool, B.mine(S.fill(part), q), Maybe.default(&2, Bool, S.look(part, q), False{}), fill_at(part, q)) :
872        {beq(_, B.mine(layout, q)) == True{} : Bool}
873      %Equal.sym(Maybe<&2, Bool>, S.look(part, q), Some{c}, me) : {beq(Maybe.default(&2, Bool, _, False{}), B.mine(layout, q)) == True{} : Bool}
874      %Equal.sym(Bool, B.mine(layout, q), c, beq_sound(B.mine(layout, q), c, cm)) : {beq(c, _) == True{} : Bool}
875      beq_refl(c)