~/jendhub

def project_right_checked

bendtorch-core@0.1.0.0 · src/shape/boundary_proofs.bend:253

import bendtorch-core@0.1.0.0/src/shape/boundary_proofs.bend as BoundaryProofs
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

253def project_right_checked(+plan: Shape.BroadcastPlan, +values: List<&2, U32>) -> {Laws.coordinate_result(Shape.right_shape(plan), Shape.project_right_checked(plan, values)) == Laws.project_right_spec(Shape.extents(Shape.left_shape(plan)), Shape.extents(Shape.right_shape(plan)), Shape.extents(Shape.output_shape(plan)), Shape.alignment(plan), Laws.decode(Shape.extents(Shape.output_shape(plan)), Shape.naturals(values))) : Maybe<&2, List<&2, U32>>}:
254  match plan:
255    case Shape.BPlan{+left, +right, +output, +alignment}:
256      project_right_ranked(left, right, output, alignment, values, Shape.bool_case(Nat.is_eq(Shape.rank_dimensions(Shape.dimensions(output)), Shape.rank_dimensions(values))))

Uses (19)

Used by (1)