TensorWindow.band_shape: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_window.bend as TensorWindow
Lines 75-80 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=75&end_line=80

import Base
import stelliferous@0.0.2.0/tensor_band.bend as Bands

# pad is both the value outside the input and the initial accumulator.
def band_shape(shape: List<&2,U32>,geometry: Bands.Geometry) -> Bool:
  match shape geometry:
    case [c,h,w] Bands.Geometry{n,ci,hi,wi}: U32.is_eq(n,1) && U32.is_eq(c,ci) && U32.is_eq(h,hi) && U32.is_eq(w,wi)
    case [n,c,h,w] Bands.Geometry{ni,ci,hi,wi}: U32.is_eq(n,ni) && U32.is_eq(c,ci) && U32.is_eq(h,hi) && U32.is_eq(w,wi)
    case shape geometry: False{}

Uses (6):
  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=List
  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_eq
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band.bend&name=Geometry