BoundaryProofs.project_left_index: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
Lines 258-276 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=258&end_line=276

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend as Coordinates
import bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend as Projection
import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
import bendtorch-core@0.1.0.0/src/shape/LAWS.bend as Laws

def project_left_index(+plan: Shape.BroadcastPlan, +map: Shape.Index<Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan))>, +index: Shape.FlatIndex<Shape.output_shape(plan)>) -> {Some{Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, map, index))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.fin_of(Shape.numel(Shape.extents(Shape.output_shape(plan))), Laws.position(Shape.output_shape(plan), index)))) : Maybe<&2, U32>}:
  match map index:
    case Shape.Indexed{+rows, +exact} Shape.FIndex{+value, +bound}:
      +left = Shape.extents(Shape.left_shape(plan))
      +right = Shape.extents(Shape.right_shape(plan))
      +output = Shape.extents(Shape.output_shape(plan))
      +fits = Coordinates.size_fits(Shape.output_shape(plan), value, bound)
      +flat = Coordinates.fin_from(Shape.numel(output), value, fits)
      +table = Shape.index_table(left, right, output)
      +projected = Shape.row_major(Shape.extents(Shape.left_shape(plan)), Shape.project_left(left, right, output, Shape.alignment(plan), Shape.unflatten(output, flat)))
      %Equal.sym(Maybe<&2, Shape.Fin(Shape.numel(output))>, Laws.fin_of(Shape.numel(output), value), Some{flat}, fin_of_from(Shape.numel(output), value, fits)) : {Some{U32.from_nat(Shape.walk_left(rows, value))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(left, right, output, Shape.alignment(plan), _)) : Maybe<&2, U32>}
      %Equal.sym(List<&2, Shape.Row>, rows, table, exact) : {Some{U32.from_nat(Shape.walk_left(_, value))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
      %Coordinates.fin_from_value(Shape.numel(output), value, fits) : {Some{U32.from_nat(Shape.walk_left(table, _))} == Some{U32.from_nat(projected)} : Maybe<&2, U32>}
      Equal.cong(Nat, Maybe<&2, U32>, flat => Some{U32.from_nat(flat)}, Shape.walk_left(table, Shape.Fin.value(Shape.numel(output), flat)), projected, Projection.walk_left_value(left, right, output, Shape.alignment(plan), flat))
    case Shape.Unindexed{zero} Shape.FIndex{+value, bound}:
      +left = Shape.extents(Shape.left_shape(plan))
      +right = Shape.extents(Shape.right_shape(plan))
      +output = Shape.extents(Shape.output_shape(plan))
      Empty.absurd({Some{Shape.index_value(Shape.left_shape(plan), Flat.project_left_index(plan, Shape.Unindexed{zero}, Shape.FIndex{value, bound}))} == Laws.flatten_spec(Shape.extents(Shape.left_shape(plan)), Laws.project_left_coordinate(left, right, output, Shape.alignment(plan), Laws.fin_of(Shape.numel(output), value))) : Maybe<&2, U32>}, Flat.hollow(Shape.output_shape(plan), value, zero, bound))

Uses (37):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=fin_of
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=flatten_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=position
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=project_left_coordinate
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fin_of_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=fin_from_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/coordinate_proofs.bend&name=size_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Fin.value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=FlatIndex
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  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=extents
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_table
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=numel
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=output_shape
  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=right_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=row_major
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=unflatten
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=walk_left
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/flat.bend&name=hollow
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/flat.bend&name=project_left_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/projection_proofs.bend&name=walk_left_value