ConstructProofs.zero_within: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend as ConstructProofs
Lines 41-46 of bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&start_line=41&end_line=46

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

def zero_within(-tail: List<&2, Nat>, +rest: Shape.Capacity<tail>) -> {True{} == within(0n <> tail, Shape.capacity.step(0n, tail, rest)) : Bool}:
  match rest:
    case Shape.Beyond{}:
      {==}
    case Shape.Within{+size, exact, bound}:
      scale_within(0n, tail, size, exact, Shape.bool_case(Bool.or(Nat.is_eq(size, 0n), Nat.is_le(0n, 1048576n))), zero_small(size), {==})

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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/construct_proofs.bend&name=scale_within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=within
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/construct_proofs.bend&name=zero_small
  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.step