def read_rebased
bendtorch-core@0.1.0.0 · src/tensor/transform_PROOF.bend:417
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
417def read_rebased(-shape: Shape.Shape, -original: Core.Tensor<shape>, -owner: Core.Tensor<shape>, +index: U32,
418 same: {owner == original : Core.Tensor<shape>}, certificate: Core.Read<shape, owner, index>) -> Core.Read<shape, original, index>:
419 Core.Read{tensor, result, exact} = certificate
420 Core.Read{tensor, result, Equal.trans(Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, (tensor, result),
421 Core.read_flat(shape, owner, index), Core.read_flat(shape, original, index), exact,
422 Equal.cong(Core.Tensor<shape>, Core.Tensor<shape> & Result<&2, &2, Core.Error, F32>, t => Core.read_flat(shape, t, index), owner, original, same))}