def unrev_true

minebender-game@1.0.0.0 · proof_laws.bend:658

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/game.bend as G

658def unrev_true(+w: Nat, +h: Nat, +shown: T.Grid(Bool), +p: T.Pos, on: {B.on_board(w, h, p) == True{} : Bool},
659  hid: {B.at(Bool, False{}, shown, p) == False{} : Bool}) -> {G.unrevealed(w, h, shown, p) == True{} : Bool}:
660  %Equal.sym(Bool, B.on_board(w, h, p), True{}, on) :
661    {Bool.and(_, Bool.not(B.at(Bool, False{}, shown, p))) == True{} : Bool}
662  %Equal.sym(Bool, B.at(Bool, False{}, shown, p), False{}, hid) : {Bool.and(True{}, Bool.not(_)) == True{} : Bool}
663  {==}