ReduceToFoldPROOF.shapes_align: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend as ReduceToFoldPROOF
Lines 51-62 of bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&start_line=51&end_line=62

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

def shapes_align(+left: Shape.Shape, +right: Shape.Shape, +left_padding: Nat, +right_padding: Nat,
  -minimal: Shape.PadMinimal<left_padding, right_padding>,
  +alignment: Shape.Alignment<Shape.pad_words(left_padding, Shape.dimensions(left)), Shape.pad_words(right_padding, Shape.dimensions(right))>) ->
  {planned_shapes(left, right, Shape.broadcast_checked.align(left, right, left_padding, right_padding, minimal, alignment)) ==
    (left, right) : Shape.Shape & Shape.Shape}:
  match alignment:
    case Shape.Misaligned{}:
      {==}
    case Shape.Aligns{+output, aligned}:
      shapes_construct(left, right, left_padding, right_padding, minimal, output,
        Shape.broadcast_checked.repad(left_padding, right_padding, Shape.dimensions(left), Shape.dimensions(right), output, aligned),
        Shape.construct(output))

Uses (13):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&name=planned_shapes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_to_fold_PROOF.bend&name=shapes_construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Alignment
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=PadMinimal
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked.align
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=broadcast_checked.repad
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=construct
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=pad_words