BroadcastProofs.project_left: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as BroadcastProofs
Lines 215-224 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=215&end_line=224

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

def project_left(+left: List<&2, Nat>, +right: List<&2, Nat>, +output: List<&2, Nat>, +alignment: Shape.Broadcast<left, right, output>, +coordinate: Shape.Coordinate(output)) -> {Shape.indices(left, Shape.project_left(left, right, output, alignment, coordinate)) == Shape.project_indices(left, Shape.indices(output, coordinate)) : List<&2, Nat>}:
  match alignment:
    case Shape.BAlign{+lp, +rp, minimal, +aligned}:
      %indices_length(output, coordinate) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(left, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, left)))) : List<&2, Nat>}
      %aligned_length_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(left, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, left)))) : List<&2, Nat>}
      %pad_length(lp, left) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(left, List.drop(&2, Nat, Shape.indices(output, coordinate), Nat.sub(_, List.length(&2, Nat, left)))) : List<&2, Nat>}
      %sub_add(lp, List.length(&2, Nat, left)) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == Shape.broadcast_indices(left, List.drop(&2, Nat, Shape.indices(output, coordinate), _)) : List<&2, Nat>}
      %drop_broadcast(lp, left, Shape.indices(output, coordinate)) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == _ : List<&2, Nat>}
      %aligned_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate) : {Shape.indices(left, Shape.unpad(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))) == List.drop(&2, Nat, _, lp) : List<&2, Nat>}
      unpad_indices(lp, left, Shape.Aligned.project_left(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_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=aligned_length_left
  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_left
  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_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unpad