def lsum
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as Naturalimport Base
79# List.sum and List.prod as right folds
80def lsum(xs: List<&2, Nat>) -> Nat:
81 match xs:
82 case Nil{}:
83 0n
84 case Con{x, t}:
85 Nat.add(x, lsum(t))
Uses (3)
Used by (6)
- bend-collections-laws-math@1.0.0.0/spec/math/generic:Sum.checked
- bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists:sum_go
- bend-collections-laws-math@1.0.0.0/proofs/math/natural/lists:sum_ok
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32int:sal
- bend-collections-laws-math@1.0.0.0/proofs/math/typed/u64int:sal
- …