def sum_ok

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/lists.bend:27

import Base
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S

27def sum_ok(+xs: List<&2, Nat>) -> {M.sum(xs) == S.lsum(xs) : Nat}:
28  sum_go(xs, 0n)