ReduceFiberProof.bound_at: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 435-442 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=435&end_line=442

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

def bound_at(-rest: List<&2, Shape.Row>, -left: Nat, -stride: Nat, +by: BoundBy<rest, left, stride>, +q: Nat,
  +below: {Nat.is_lt(q, stride) == True{} : Bool}) -> {Nat.is_lt(Shape.walk_left(rest, q), left) == True{} : Bool}:
  BoundBy{+lt, +rt, +ot, +aligned, +rows, +size, +count} = by
  %rows : {Nat.is_lt(Shape.walk_left(_, q), left) == True{} : Bool}
  %size : {Nat.is_lt(Shape.walk_left(Shape.index_rows(lt, rt, ot), q), _) == True{} : Bool}
  walk_left_below(lt, rt, ot, aligned, q,
    %Equal.sym(Nat, Shape.numel(ot), stride, count) : {Nat.is_lt(q, _) == True{} : Bool}
    below)

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=BoundBy
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=walk_left_below
  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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left