def prefix_checked_case

bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:330

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

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