BoundaryProofs.project_left_fits: def of bendtorch-core@0.1.0.0 Import: import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs Lines 193-205 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=193&end_line=205 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/LAWS.bend as Laws def project_left_fits(+left: Shape.Shape, +right: Shape.Shape, +output: Shape.Shape, +alignment: Shape.Broadcast, +values: List<&2, U32>, +verdict: Shape.BoolCase) -> {Laws.coordinate_result(left, Shape.projection_checked.fits(left, output, values, verdict)) == Laws.project_left_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 verdict: case Shape.BFalse{equal}: %decode_unfit(Shape.extents(output), Shape.naturals(values), fit_words_false(Shape.dimensions(output), values, equal)) : {None{} == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>} {==} case Shape.BTrue{equal}: +fits = Coordinates.fits_of(Shape.extents(output), Shape.naturals(values), fit_words_true(Shape.dimensions(output), values, equal)) +coordinate = Coordinates.coordinate_of(Shape.extents(output), Shape.naturals(values), fits) +projected = 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(Maybe<&2, Shape.Coordinate(Shape.extents(output))>, Laws.decode(Shape.extents(output), Shape.naturals(values)), Some{coordinate}, decode_fit(Shape.extents(output), Shape.naturals(values), fits)) : {Laws.coordinate_result(left, Shape.coordinate_checked.nat(left, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)))) == Laws.project_left_spec(Shape.extents(left), Shape.extents(right), Shape.extents(output), alignment, _) : Maybe<&2, List<&2, U32>>} %Equal.sym(List<&2, Nat>, Shape.projected_words(Shape.dimensions(left), List.drop(&2, U32, values, count)), Shape.indices(Shape.extents(left), projected), projected_left(left, right, output, alignment, values, fits)) : {Laws.coordinate_result(left, Shape.coordinate_checked.nat(left, _)) == Some{Shape.words(Shape.indices(Shape.extents(left), projected))} : Maybe<&2, List<&2, U32>>} checked_indices(left, projected) Uses (33): 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=Maybe 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/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_left_spec https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=checked_indices https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_fit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=decode_unfit https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fit_words_false https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=fit_words_true https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend&name=projected_left 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=fits_of 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=Coordinate 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=coordinate_checked.nat 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=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_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=projection_checked.fits 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=words