ProjectionPROOF.checked_acceptance: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/projection_PROOF.bend as ProjectionPROOF
Lines 58-67 of bendtorch-core@0.1.0.0/src/tensor/projection_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_PROOF.bend&start_line=58&end_line=67

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

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

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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/coordinate_proofs.bend&name=size_misses
  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=BroadcastPlan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=elements
  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=flat_checked.finish
  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/tensor/elementwise.bend&name=flat_input_indices
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/projection_LAWS.bend&name=indices_accepted