ReduceFiberProof.block: 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 536-545 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=536&end_line=545

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/storage/api.bend as Api

# The first block of a row, at cursor digit * stride: the rows below at
# base + right * digit.
def block(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +inner: Nat, +base: Nat, +digit: Nat,
  +mode: MaskMode<left, digit, target, inner>) ->
  {masked(stride, Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) ==
    masked(stride, rest, inner, Nat.add(base, Nat.mul(right, digit)), 0n) : List<&2, Nat>}:
  %Broadcast.add_zero(Nat.mul(digit, stride)) :
    {masked(stride, Shape.Row{stride, left, right} <> rest, target, base, _) ==
      masked(stride, rest, inner, Nat.add(base, Nat.mul(right, digit)), 0n) : List<&2, Nat>}
  shifted(stride, stride, left, right, rest, target, inner, base, digit, 0n, Api.le_refl(stride), mode)

Uses (10):
  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.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=MaskMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=shifted
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_zero
  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/storage/api.bend&name=le_refl