def checked_acceptance

bendtorch-core@0.1.0.0 · src/tensor/projection_PROOF.bend:58

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/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend as Laws

58def checked_acceptance(+plan: Shape.BroadcastPlan, +position: Nat,
59  decision: Shape.BoolCase<Nat.is_lt(position, Shape.elements(Shape.output_shape(plan)))>) ->
60  {Laws.indices_accepted(Elementwise.flat_input_indices(plan,
61    Shape.flat_checked.finish(Shape.output_shape(plan), position, decision))) ==
62    Nat.is_lt(position, Shape.numel(Shape.extents(Shape.output_shape(plan)))) : Bool}:
63  match decision:
64    case Shape.BFalse{equal}:
65      Coordinates.size_misses(Shape.output_shape(plan), position, equal)
66    case Shape.BTrue{equal}:
67      Coordinates.size_fits(Shape.output_shape(plan), position, equal)