def capacity.step

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

import Base

590# A size is formed only when the suffix size is zero or both factors are at
591# most 2^20, so no product exceeds 2^40, below the native Nat limit of 2^48.
592def capacity.step(+head: Nat, -tail: List<&2, Nat>, rest: Capacity<tail>) -> Capacity<head <> tail>:
593  match rest:
594    case Beyond{}:
595      capacity.zero(head, tail)
596    case Within{+size, exact, bound}:
597      capacity.scale(head, tail, size, exact, bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(head, 1048576n))))