BoundaryProofs.projected_left: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 182-191 of bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&start_line=182&end_line=191

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend as Broadcast
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates

def projected_left(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast<Shape.extents(left), Shape.extents(right), Shape.extents(output)>, +values: List<&2, U32>, +fits: Coordinates.Fits(Shape.extents(output), Shape.naturals(values))) -> {Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(left))))) == Shape.indices(Shape.extents(left), Shape.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits))) : List<&2, Nat>}:
  +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits)
  +expected = Shape.indices(Shape.extents(left), Shape.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))
  +count = Nat.sub(Shape.rank_dimensions(values), Shape.rank_dimensions(Shape.dimensions(left)))
  %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)), Shape.broadcast_indices(Shape.extents(left), Shape.naturals(List.drop(&2, U32, values, count))), Coordinates.projected_words_spec(Shape.dimensions(left), List.drop(&2, U32, values, count))) : {_ == expected : List<&2, Nat>}
  %Equal.sym(List<&2, Nat>, Shape.naturals(List.drop(&2, U32, values, count)), List.drop(&2, Nat, Shape.naturals(values), count), Coordinates.naturals_drop(values, count)) : {Shape.broadcast_indices(Shape.extents(left), _) == expected : List<&2, Nat>}
  %Equal.sym(Nat, Shape.rank_dimensions(values), List.length(&2, Nat, Shape.naturals(values)), Shape.rank_naturals(values)) : {Shape.broadcast_indices(Shape.extents(left), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(_, Shape.rank_dimensions(Shape.dimensions(left))))) == expected : List<&2, Nat>}
  %Equal.sym(Nat, Shape.rank_dimensions(Shape.dimensions(left)), List.length(&2, Nat, Shape.extents(left)), Shape.rank_naturals(Shape.dimensions(left))) : {Shape.broadcast_indices(Shape.extents(left), List.drop(&2, Nat, Shape.naturals(values), Nat.sub(List.length(&2, Nat, Shape.naturals(values)), _))) == expected : List<&2, Nat>}
  %Coordinates.indices_of(Shape.extents(output), Shape.naturals(values), fits) : {Shape.project_indices(Shape.extents(left), _) == expected : List<&2, Nat>}
  Equal.sym(List<&2, Nat>, expected, Shape.project_indices(Shape.extents(left), Shape.indices(Shape.extents(output), coordinate)), Broadcast.project_left(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, coordinate))

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Base/base.bend&name=U32
  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/coordinate_proofs.bend&name=Fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=coordinate_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=indices_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=naturals_drop
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=projected_words_spec
  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=Shape
  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=dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=extents
  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=naturals
  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=projected_words
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_naturals