TensorOperations.sweep_geometry: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_operations.bend as TensorOperations
Lines 209-214 of stelliferous@0.0.2.0/tensor_operations.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_operations.bend&start_line=209&end_line=214

import Base
import stelliferous@0.0.2.0/tensor_access.bend as Access

# The window geometry of a whole axis is exact and every sample address stays in U32.
def sweep_geometry(+sweep: Access.Sweep) -> Bool:
  Access.Sweep{+extent,+step,+kernel,+stride,+padding,+out_extent,+origin} = sweep
  small(extent) && small(kernel) && small(stride) && small(padding) && U32.is_lt(0,kernel) && U32.is_lt(0,stride) && U32.is_lt(0,step) &&
    U32.is_eq(origin,0) && U32.is_le(kernel,(extent + 2 * padding : U32)) &&
    U32.is_eq(out_extent,((extent + 2 * padding - kernel : U32) / stride + 1 : U32))

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.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=Sweep
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_operations.bend&name=small