def project_left
bendtorch-core@0.1.0.0 · src/shape/broadcast_proofs.bend:215
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
215def 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>}:
216 match alignment:
217 case Shape.BAlign{+lp, +rp, minimal, +aligned}:
218 %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>}
219 %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>}
220 %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>}
221 %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>}
222 %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>}
223 %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>}
224 unpad_indices(lp, left, Shape.Aligned.project_left(Shape.pad(lp, left), Shape.pad(rp, right), output, aligned, coordinate))