def source_value

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

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

427def source_value(-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>, +index: U32, +value: F32,
428  -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
429  certificate: Core.SourceRead<shape, original, index>) -> SourceValue<shape, original, index, value>:
430  Core.SourceRead{meaning} = certificate
431  SourceValue{Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, original, index),
432    Core.read_value(shape, Core.read_flat(shape, original, index)), Some{value},
433    Equal.sym(Maybe<&2, F32>, Core.read_value(shape, Core.read_flat(shape, original, index)), Core.checked_observe(shape, original, index), meaning),
434    Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.read_value(shape, pair),
435      Core.read_flat(shape, original, index), (retained, Done{value}),
436      Equal.sym(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, (retained, Done{value}), Core.read_flat(shape, original, index), exact)))}