CorePROOF.checked_update_pair: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend as CorePROOF
Lines 468-490 of bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&start_line=468&end_line=490

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

def checked_update_pair(-shape: Shape.Shape, -original: Core.Tensor<shape>, +index: U32, +value: F32,
  pair: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>, -meaning: Core.UpdateMeaning(shape, original, index, value, pair)) ->
  CheckedUpdatePair<shape, original, index, value, pair>:
  (output, result) = pair
  match result:
    case Fail{error}:
      CheckedUpdatePair{Unit{}}
    case Done{unit}:
      CheckedUpdatePair{(update_route(shape, original, output, index, value, unit, meaning),
        (Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, output, index), Core.observe(shape, output, index), Some{value},
          {\{Core.ObservationModel: equal => equal} :
            Core.ObservationModel<shape, output, index, update_route(shape, original, output, index, value, unit, meaning)> ->
              {Core.checked_observe(shape, output, index) == Core.observe(shape, output, index) : Maybe<&2, F32>}}(Core.observation_model(shape, output, index, update_route(shape, original, output, index, value, unit, meaning))),
          update_value(shape, original, output, index, value, unit, meaning)),
          other => checked => different =>
            {\{Tuple: after => physical => (after,
              {\{CheckedFrame: equal => equal} : CheckedFrame<shape, original, output, other> ->
                {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>}}(checked_frame(shape, original, output, other, checked, after, physical)))
            } :
              (Core.ObservationChecked(Core.Packed{shape, output}, other) &
                {Core.observe(shape, output, other) == Core.observe(shape, original, other) : Maybe<&2, F32>}) ->
              (Core.ObservationChecked(Core.Packed{shape, output}, other) &
                {Core.checked_observe(shape, output, other) == Core.checked_observe(shape, original, other) : Maybe<&2, F32>})}(update_frame(shape, original, output, index, value, unit, meaning)(other)(checked)(different))))}

Uses (24):
  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=Maybe
  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=Unit
  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=Error
  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=ObservationModel
  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=UpdateMeaning
  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=observation_model
  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/core_PROOF.bend&name=CheckedFrame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=CheckedUpdatePair
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=checked_frame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_frame
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_route
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/core_PROOF.bend&name=update_value