def Witness

minebender-game@1.0.0.0 · proof_solver.bend:2186

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

2186# A layout that passes the check and mines c.
2187def Witness(+ctx: S.Ctx, +c: T.Pos) -> Type:
2188  Exists(T.Grid(Bool), l => {S.check(ctx, l) == True{} : Bool} & {B.mine(l, c) == True{} : Bool})