TransformPROOF.prefix_checked_case: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 330-342 of bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&start_line=330&end_line=342

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core

def prefix_checked_case(-input: Shape.Shape, -axes: List<&2, U32>, -plan: Layout.Plan<input, axes>,
  -target: Core.Tensor<Layout.output(input, axes, plan)>, -cursor: Nat, +other: Nat,
  prior: @+j: Nat -> @-earlier: {Nat.is_lt(j, cursor) == True{} : Bool} ->
    Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(j)),
  current: Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(cursor)),
  split: Either<&2, &2, {Nat.is_lt(other, cursor) == True{} : Bool}, {other == cursor : Nat}>) ->
  Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(other)):
  match split:
    case Inl{earlier}:
      prior(other, earlier)
    case Inr{equal}:
      %Equal.sym(Nat, other, cursor, equal) : Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, U32.from_nat(_))
      current

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=Either
  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=Nat
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  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/tensor/core.bend&name=Dynamic
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=ObservationChecked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=Tensor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=Plan
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/layout.bend&name=output