def zero_within

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

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

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