LAWS.broadcast_left_projection: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as LAWS
Lines 144-150 of bendtorch-core@0.1.0.0/src/shape/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&start_line=144&end_line=150

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

law broadcast_left_projection:
  for +left: List<&2, Nat>
  for +right: List<&2, Nat>
  for +output: List<&2, Nat>
  for +alignment: Shape.Broadcast<left, right, output>
  for +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>}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=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=indices
  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