def product

bend-ml-nat-lemmas@0.1.2.0 · main.bend:17

import Base

17# Product of the elements of a list of Nat; the empty list is 1.
18# It is the "number of elements" of a tensor whose shape is the list.
19def product(xs: List<&2, Nat>) -> Nat:
20  match xs:
21    case Nil{}:
22      1n
23    case Con{h, t}:
24      Nat.mul(h, product(t))