TransformPROOF.prefix_observation: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
Lines 2234-2253 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=2234&end_line=2253

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
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend as WordConversion
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

def prefix_observation(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>,
  -original: Core.Tensor<input>, -retained: Core.Tensor<input>, -target: Core.Tensor<Layout.output(input, axes, plan)>, +index: U32,
  -prefix: Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))>,
  -inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))) == True{} : Bool}) ->
  Totality.CopyObservation<input, axes, plan, original, target, index>:
  Totality.CopyObservation{
    {\{Transforms.Prefix: kept => words => checked => written =>
      Equal.trans(Maybe<&2, F32>, Core.observe(Layout.output(input, axes, plan), target, index), Core.checked_observe(Layout.output(input, axes, plan), target, index),
        Transforms.expected_output(input, axes, plan, original, index),
        {\{ObserveBridge: equal => Equal.sym(Maybe<&2, F32>, Core.checked_observe(Layout.output(input, axes, plan), target, index), Core.observe(Layout.output(input, axes, plan), target, index), equal)} :
          ObserveBridge<Layout.output(input, axes, plan), target, index> ->
            {Core.observe(Layout.output(input, axes, plan), target, index) == Core.checked_observe(Layout.output(input, axes, plan), target, index) : Maybe<&2, F32>}}(
              observe_bridge(Layout.output(input, axes, plan), target, index,
                %WordConversion.word_natural_exact(index) : Core.ObservationChecked(Core.Packed{Layout.output(input, axes, plan), target}, _)
                checked(U32.to_nat(index), inside))),
        %WordConversion.word_natural_exact(index) :
          {Core.checked_observe(Layout.output(input, axes, plan), target, _) == Transforms.expected_output(input, axes, plan, original, _) : Maybe<&2, F32>}
        written(U32.to_nat(index), inside))} :
          Transforms.Prefix<input, axes, plan, original, retained, target, Shape.logical_numel(Shape.dimensions(Layout.output(input, axes, plan)))> ->
            {Core.observe(Layout.output(input, axes, plan), target, index) == Transforms.expected_output(input, axes, plan, original, index) : Maybe<&2, F32>}}(prefix)}

Uses (25):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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.to_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/shape/core.bend&name=dimensions
  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/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/core.bend&name=checked_observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core.bend&name=observe
  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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=ObserveBridge
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend&name=observe_bridge
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend&name=CopyObservation
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=Prefix
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/transforms.bend&name=expected_output
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/word_conversion.bend&name=word_natural_exact