def project_right
bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:226
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
226def project_right(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>, +coordinate: Shape.Coordinate(output)) -> {Shape.indices(right, Shape.project_right(left, right, output, alignment, coordinate)) == Shape.project_indices(right, Shape.indices(output, coordinate)) : List<&2, Nat>}:
227 match alignment:
228 case Shape.BAlign{+lp, +rp, minimal, +aligned}:
229 %indices_length(output, coordinate) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(right, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, right)))) : List<&2, Nat>}
230 %aligned_length_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(right, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, right)))) : List<&2, Nat>}
231 %pad_length(rp, right) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(right, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, right)))) : List<&2, Nat>}
232 %sub_add(rp, List.length(&2, Nat, right)) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(right, List.drop(&2, Nat, Shape.indices(output, coordinate), _)) : List<&2, Nat>}
233 %drop_broadcast(rp, right, Shape.indices(output, coordinate)) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == _ : List<&2, Nat>}
234 %aligned_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate) : {Shape.indices(right, Shape.unpad(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == List.drop(&2, Nat, _, rp) : List<&2, Nat>}
235 unpad_indices(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))