def untouched_value

bendtorch-core@0.1.0.0 · src/tensor/clone_contract.bend:26

import bendtorch-core@0.1.0.0/src/tensor/clone_contract.bend as CloneContract
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
import bendtorch-core@0.1.0.0/src/tensor/observation.bend as Observation

26def untouched_value(-shape: Shape.Shape, +other: U32, written: Core.Tensor<shape> & Result<&2, &2, Core.Error, Unit>,
27  storage: Storage.Storage, -valid: {Lifecycle.logical_length(storage) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}) ->
28  {Observation.untouched(shape, other, written, Core.TTensor{storage, valid}) == Lifecycle.read_value(Storage.get(storage, other)) : Maybe<&2, F32>}:
29  (tensor, result) = written
30  Core.read_result_value(shape, storage, valid, other, Storage.get(storage, other), {==})

Uses (19)

Used by (1)