BroadcastProofs.project_right: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
Lines 226-235 of bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&start_line=226&end_line=235

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

def 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>}:
  match alignment:
    case Shape.BAlign{+lp, +rp, minimal, +aligned}:
      %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>}
      %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>}
      %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>}
      %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>}
      %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>}
      %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>}
      unpad_indices(rp, right, Shape.Aligned.project_right(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))

Uses (21):
  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=aligned_length_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=aligned_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=drop_broadcast
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=indices_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=pad_length
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=unpad_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Aligned.project_right
  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=Coordinate
  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=indices
  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_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unpad