ReduceFiberProof.fiber_cons: 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 822-844 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=822&end_line=844

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/arith.bend as Arith

def fiber_cons(+lh: Nat, +lt: List<&2, Nat>, +rh: Nat, +rt: List<&2, Nat>, +oh: Nat, +ot: List<&2, Nat>, +axis: Shape.Axis<lh, rh, oh>,
  +tail: Shape.Aligned(lt, rt, ot), +target: Nat, +below: {Nat.is_lt(target, Nat.mul(lh, Shape.numel(lt))) == True{} : Bool},
  rec: @+inner: Nat -> @+inside: {Nat.is_lt(inner, Shape.numel(lt)) == True{} : Bool} -> RowsWalk(lt, rt, ot, inner)) ->
  RowsWalk(lh <> lt, rh <> rt, oh <> ot, target):
  match lh:
    case 0n:
      Empty.absurd(RowsWalk(0n <> lt, rh <> rt, oh <> ot, target), Arith.lt_zero(target, below))
    case 1n+k:
      match k:
        case 0n:
          reduced_blocks(oh, Shape.numel(ot), Shape.broadcast_index(rh, Shape.numel(rt)), Shape.index_rows(lt, rt, ot), oh, ot, target, 0n, 0n,
            rec(target,
              %Broadcast.add_zero(Shape.numel(lt)) : {Nat.is_lt(target, _) == True{} : Bool}
              below))
        case 1n+j:
          +size = Shape.numel(lt)
          kept_row(size, Shape.numel(ot), Shape.broadcast_index(rh, Shape.numel(rt)), Shape.index_rows(lt, rt, ot), oh, ot, target, 0n,
            %Equal.sym(Nat, oh, 2n+j, axis_kept(j, rh, oh, axis)) : {Nat.is_lt(target, Nat.mul(_, size)) == True{} : Bool}
            below,
            rec(Nat.mod(target, size),
              {\{Decomposed: m_below => sum => m_below} : Decomposed<target, size> -> {Nat.is_lt(Nat.mod(target, size), size) == True{} : Bool}}(
                decompose(target, size, positive_of(target, 2n+j, size, below)))),
            BoundBy{lt, rt, ot, tail, {==}, {==}, {==}})

Uses (23):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=Base/base.bend&name=Nat.mod
  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=BoundBy
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=Decomposed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RowsWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=axis_kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=decompose
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept_row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=positive_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=reduced_blocks
  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=Aligned
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Axis
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_index
  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/storage/arith.bend&name=lt_zero