ElementwisePROOF.checked_indices_success: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend as ElementwisePROOF
Lines 614-632 of bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&start_line=614&end_line=632

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/elementwise.bend as Elementwise
import bendtorch-core@0.1.0.0/src/shape/flat.bend as Flat
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

def checked_indices_success(+plan: Shape.BroadcastPlan, +index: U32,
  decision: Shape.BoolCase<Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan)))>,
  -inside: {Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))) == True{} : Bool}) ->
  IndicesDone<plan, Elementwise.flat_input_indices(plan, Shape.flat_checked.finish(Shape.output_shape(plan), U32.to_nat(index), decision))>:
  match decision:
    case Shape.BFalse{equal}:
      IndicesDone{0, 0,
        Empty.absurd({Done{(0, 0)} == Fail{Core.ShapeError{Shape.FlatIndexOutOfBounds{}}} : Result<&2, &1, Core.Error, U32 & U32>},
          Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside))),
        Empty.absurd({Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.left_shape(plan)))) == True{} : Bool},
          Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside))),
        Empty.absurd({Nat.is_lt(0n, Shape.logical_numel(Shape.dimensions(Shape.right_shape(plan)))) == True{} : Bool},
          Arith.clash(Equal.trans(Bool, False{}, Nat.is_lt(U32.to_nat(index), Shape.elements(Shape.output_shape(plan))), True{}, equal, inside)))}
    case Shape.BTrue{equal}:
      +flat = {Shape.FIndex{U32.to_nat(index), equal} : Shape.FlatIndex<Shape.output_shape(plan)>}
      +left = Flat.project_left_index(plan, Shape.index_map(plan), flat)
      +right = Flat.project_right_index(plan, Shape.index_map(plan), flat)
      IndicesDone{Shape.index_value(Shape.left_shape(plan), left), Shape.index_value(Shape.right_shape(plan), right), {==},
        flat_index_inside(Shape.left_shape(plan), left), flat_index_inside(Shape.right_shape(plan), right)}

Uses (29):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Result
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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=Error
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=FlatIndex
  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=elements
  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=index_map
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=index_value
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=left_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=logical_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/shape/core.bend&name=right_shape
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/flat.bend&name=project_left_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/flat.bend&name=project_right_index
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=clash
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Error
  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/elementwise_PROOF.bend&name=IndicesDone
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_PROOF.bend&name=flat_index_inside