Function Product

lean_py/z3/core.py:1693–1706

Left-fold product.

(*args: ArithRef)

def Product(*args: ArithRef) -> ArithRef:
    """Left-fold product."""
    flat: list[ArithRef] = []
    for a in args:
        if isinstance(a, (list, tuple)):
            flat.extend(a)
        else:
            flat.append(a)
    if not flat:
        return IntVal(1)
    result = flat[0]
    for a in flat[1:]:
        result = result * a
    return result


# ---------------------------------------------------------------------------