law row_mines_sum

minebender-game@1.0.0.0 · proof_solver.bend:30

import Base
import minebender-game@1.0.0.0/board.bend as B
import minebender-game@1.0.0.0/proof_sums.bend as PU

30law row_mines_sum:
31  for +r: List<&2, Bool>
32  {B.row_mines(r) == PU.rsum(~Bool, ~one, r) : Nat}