ReduceFiberProof.BoundBy: type of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 427-433 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=427&end_line=433

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

# Below a kept row of left stride `left`, every walk of the rows below
# stays under `left`: the rows are the index rows of an aligned broadcast
# whose left count is `left` and whose output count is `stride`.
type BoundBy<-rest: List<&2, Shape.Row>, -left: Nat, -stride: Nat> is Data:
  BoundBy{lt: List<&2, Nat>, rt: List<&2, Nat>, ot: List<&2, Nat>, aligned: Shape.Aligned(lt, rt, ot),
    rows: {Shape.index_rows(lt, rt, ot) == rest : List<&2, Shape.Row>},
    size: {Shape.numel(lt) == left : Nat}, count: {Shape.numel(ot) == stride : Nat}}

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel