law grid_sum

minebender-game@1.0.0.0 · proof_sums.bend:261

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

261# Summing over a w-by-h grid row by row equals summing over its cells.
262law grid_sum:
263  for ~A: Data
264  for ~f: A -> Nat
265  for +d: A
266  for +w: Nat
267  for +h: Nat
268  for +g: T.Grid(A)
269  for +sh: {B.shaped(A, w, h, g) == True{} : Bool}
270  {csum(~A, ~f, d, g, B.cells(w, h)) == gsum(~A, ~f, g) : Nat}