def capacity.scale

bendtorch-core@0.1.0.0 · src/shape/core.bend:575

import Base

575def capacity.scale(+head: Nat, -tail: List<&2, Nat>, +size: Nat, exact: {size == numel(tail) : Nat}, small: BoolCase<Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n))>) -> Capacity<head <> tail>:
576  match small:
577    case BFalse{equal}:
578      Beyond{}
579    case BTrue{equal}:
580      +product = Nat.mul(head, size)
581      capacity.bound(head <> tail, product, Equal.cong(Nat, Nat, value => Nat.mul(head, value), size, numel(tail), exact), bool_case(Nat.is_le(product, 1048576n)))