def ProvablySafe

minebender-game@1.0.0.0 · LAWS.bend:176

import Base
import minebender-game@1.0.0.0/types.bend as T

176# p is hidden, and no layout consistent with what the player knows has a mine on p.
177def ProvablySafe(v: T.Knowledge, p: T.Pos) -> Type:
178  {hidden(v, p) == True{} : Bool} &
179  (@layout: T.Grid(Bool) ->
180    {consistent(v, layout) == True{} : Bool} ->
181    {mine(layout, p) == False{} : Bool})