TensorBandPool.window_size: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/tensor_band_pool.bend as TensorBandPool
Lines 21-23 of stelliferous@0.0.2.0/tensor_band_pool.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/tensor_band_pool.bend&start_line=21&end_line=23

import Base
import stelliferous@0.0.2.0/tensor_band_window.bend as BandWindow
import stelliferous@0.0.2.0/tensor_band_schedule.bend as BandSchedule

def window_size(window: BandWindow.RowWindow) -> BandSchedule.Size:
  BandWindow.RowWindow{BandWindow.Rows{first,+count},above,below,rows} = window
  BandSchedule.Size{1,count,count}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band_schedule.bend&name=Size
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band_window.bend&name=RowWindow
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/tensor_band_window.bend&name=Rows