def rsum_at

minebender-game@1.0.0.0 · proof_sums.bend:79

import Base

79def rsum_at(~A: Data, ~f: A -> Nat, +d: A, +r: List<&2, A>, xs: List<&2, Nat>) -> Nat:
80  match xs:
81    case Nil{}:
82      0n
83    case x <> t:
84      Nat.add(f(Maybe.default(&2, A, List.get(&2, A, r, x), d)), rsum_at(~A, ~f, d, r, t))