law total_sum

minebender-game@1.0.0.0 · proof_solver.bend:42

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/proof_sums.bend as PU

42law total_sum:
43  for +g: T.Grid(Bool)
44  {B.total_mines(g) == PU.gsum(~Bool, ~one, g) : Nat}