ProjectionProofs.walk_left_value: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as ProjectionProofs Lines 132-148 of bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&start_line=132&end_line=148 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/shape/coordinate_proofs.bend as Coordinates def walk_left_value(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast, +index: Shape.Fin(Shape.numel(output))) -> {Shape.walk_left(Shape.index_table(left, right, output), Shape.Fin.value(Shape.numel(output), index)) == Shape.row_major(left, Shape.project_left(left, right, output, alignment, Shape.unflatten(output, index))) : Nat}: +value = Shape.Fin.value(Shape.numel(output), index) +ds = Shape.digits(output, value) +nl = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, left)) +nr = Nat.sub(List.length(&2, Nat, output), List.length(&2, Nat, right)) +coordinate = Shape.unflatten(output, index) +projected = Shape.project_left(left, right, output, alignment, coordinate) +strides = strides_of(left) +dropped = List.drop(&2, Nat, ds, nl) %Equal.sym(Nat, Shape.walk_left(Shape.index_rows(Shape.pad(nl, left), Shape.pad(nr, right), output), value), dot(strides_of(Shape.pad(nl, left)), ds), walk_left_rows(Shape.pad(nl, left), Shape.pad(nr, right), output, value, right_padded(left, right, output, alignment))) : {_ == Shape.row_major(left, projected) : Nat} %Equal.cong(List<&2, Nat>, Nat, steps => dot(steps, ds), zeros(nl, strides), strides_of(Shape.pad(nl, left)), Equal.sym(List<&2, Nat>, strides_of(Shape.pad(nl, left)), zeros(nl, strides), pad_strides(nl, left))) : {_ == Shape.row_major(left, projected) : Nat} %Equal.sym(Nat, dot(zeros(nl, strides), ds), dot(strides, dropped), dot_zeros(nl, ds, strides)) : {_ == Shape.row_major(left, projected) : Nat} %Equal.sym(Nat, dot(strides, dropped), Shape.offset(left, Shape.broadcast_indices(left, dropped)), dot_broadcast(left, dropped)) : {_ == Shape.row_major(left, projected) : Nat} %Equal.cong(Nat, Nat, width => Shape.offset(left, Shape.broadcast_indices(left, List.drop(&2, Nat, ds, Nat.sub(width, List.length(&2, Nat, left))))), List.length(&2, Nat, ds), List.length(&2, Nat, output), digits_length(output, value)) : {_ == Shape.row_major(left, projected) : Nat} %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(left, Shape.project_indices(left, values)), Shape.indices(output, coordinate), ds, Coordinates.digits_unflatten(output, index)) : {_ == Shape.row_major(left, projected) : Nat} %Equal.cong(List<&2, Nat>, Nat, values => Shape.offset(left, values), Shape.indices(left, projected), Shape.project_indices(left, Shape.indices(output, coordinate)), Broadcast.project_left(left, right, output, alignment, coordinate)) : {_ == Shape.row_major(left, projected) : Nat} Coordinates.offset_indices(left, projected) Uses (35): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong 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=List.drop https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=project_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=digits_unflatten https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=offset_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Broadcast https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=digits 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=index_table https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=indices 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=offset https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=project_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=project_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=digits_length https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot_broadcast https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=dot_zeros https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=pad_strides https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=right_padded https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=strides_of https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=walk_left_rows https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=zeros