def gsum

minebender-game@1.0.0.0 · proof_sums.bend:63

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

63# The sum of f over the grid, row by row.
64def gsum(~A: Data, ~f: A -> Nat, g: T.Grid(A)) -> Nat:
65  match g:
66    case Nil{}:
67      0n
68    case r <> t:
69      Nat.add(rsum(~A, ~f, r), gsum(~A, ~f, t))