Core.capacity.step: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/core.bend as Core
Lines 590-597 of bendtorch-core@0.1.0.0/src/shape/core.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&start_line=590&end_line=597

import Base

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

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.or
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Capacity
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=capacity.scale
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=capacity.zero