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

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

def project_right_ranked(+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>, +same: Shape.BoolCase<Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))>) -> {Laws.coordinate_result(right, Shape.projection_checked.ranked(right, output, values, same)) == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, Laws.decode(Shape.extents(output), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
  match same:
    case Shape.BFalse{equal}:
      %decode_rank(Shape.dimensions(output), values, equal) : {None{} == Laws.project_right_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>}
      {==}
    case Shape.BTrue{equal}:
      project_right_fits(left, right, output, alignment, values, Shape.bool_case(Shape.fit_words(Shape.dimensions(output), values)))

Uses (19):
  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.is_eq
  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/LAWS.bend&name=coordinate_result
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=decode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/LAWS.bend&name=project_right_spec
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_rank
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=project_right_fits
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=BoolCase
  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=bool_case
  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=fit_words
  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=projection_checked.ranked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=rank_dimensions