def source_kept
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:441
import bendtorch-core@0.1.0.0/src/tensor/transform_PROOF.bend as TransformPROOF
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
441def source_kept(-shape: Shape.Shape, -original: Core.Tensor<shape>, -retained: Core.Tensor<shape>, +index: U32, -value: F32,
442 -exact: {(retained, Done{value}) == Core.read_flat(shape, original, index) : Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>},
443 certificate: Core.SourceReadKeeps<shape, original, index>) -> SourceKept<shape, original, retained>:
444 Core.SourceReadKeeps{kept} = certificate
445 SourceKept{other => Equal.trans(Maybe<&2, F32>, Core.checked_observe(shape, retained, other),
446 Core.retained_read_observe(shape, Core.read_flat(shape, original, index), other), Core.checked_observe(shape, original, other),
447 Equal.cong(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, Maybe<&2, F32>, pair => Core.retained_read_observe(shape, pair, other),
448 (retained, Done{value}), Core.read_flat(shape, original, index), exact), kept(other))}