~/jendhub

law mark_ok

minebender-game@1.0.0.0 · proof_display.bend:251

import minebender-game@1.0.0.0/proof_display.bend as ProofDisplay
import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G
import minebender-game@1.0.0.0/LAWS.bend as L

251# What the end of the game singles out is never covered.
252law mark_ok:
253  for +st: T.Status
254  for +p: T.Pos
255  {Maybe.default(&2, Bool, Maybe.map(&2, T.Tile, Bool, t => L.is_covered(t), G.mark(st, p)), False{}) == False{} : Bool}

Uses (9)

Used by (1)