def prod_value

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/proof.bend:80

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/lists.bend as LS

80def prod_value(+xs: List<&2, Nat>) -> S.Prod.value(xs):
81  LS.prod_ok(xs)