TensorWindow.band_geometry: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_window.bend as TensorWindow
Lines 99-105 of stelliferous@0.0.2.0/tensor_window.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_window.bend&start_line=99&end_line=105

import Base
import stelliferous@0.0.2.0/tensor_shape.bend as Shapes
import stelliferous@0.0.2.0/tensor_access.bend as Access
import stelliferous@0.0.2.0/tensor_operations.bend as Operations
import stelliferous@0.0.2.0/tensor.bend as Tensors
import stelliferous@0.0.2.0/tensor_band.bend as Bands

def band_geometry(~Element: Data,~operation: Element -> Element -> Element,name: String,pad: Element,+pool: Access.Pool,+geometry: Bands.Geometry,bands: Bands.Bands(~Element),
  +shape: List<&2,U32>,fill: Element,workers: U32) -> Tensors.Tensor<Element>:
  Access.Pool{+height,+width,+kernel,+stride,+padding,+out_height,+out_width} = pool
  +pool = {Access.Pool{height,width,kernel,stride,padding,out_height,out_width} : Access.Pool}
  +out_shape = List.append(&2,U32,List.take(&2,U32,shape,Nat.sub(List.length(&2,U32,shape),2n)),[out_height,out_width])
  band_count(~Element,~operation,name,band_shape(shape,geometry) && Operations.pool_geometry(pool) && U32.is_lt(0,height) && U32.is_lt(0,width) &&
    Bool.not(Shapes.has_zero(out_shape)),Tensors.count_of(middle_shape(shape,pool)),Tensors.count_of(out_shape),pad,pool,geometry,bands,shape,out_shape,fill,workers)

Uses (20):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.take
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor.bend&name=count_of
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_access.bend&name=Pool
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band.bend&name=Bands
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band.bend&name=Geometry
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_operations.bend&name=pool_geometry
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_shape.bend&name=has_zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_window.bend&name=band_count
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_window.bend&name=band_shape
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_window.bend&name=middle_shape