def prod_go

bend-collections-laws-crypto@1.0.0.0 · spec/math/generic.bend:119

import bend-collections-laws-crypto@1.0.0.0/spec/math/generic.bend as Generic
import Base

119# a fold that stops at the first prefix of w bits or more (prod, lcm_all:
120# a later 0 can shrink the value, the overflow already happened)
121def prod_go(+w: Nat, xs: List<&2, Nat>, +acc: Nat, ok: Bool) -> Nat & Bool:
122  match xs ok:
123    case Nil{} _:
124      (acc, ok)
125    case Con{x, t} False{}:
126      (acc, False{})
127    case Con{+x, t} True{}:
128      prod_go(w, t, Nat.mul(acc, x), fits(w, Nat.mul(acc, x)))

Uses (7)

Used by (1)