def value_after_read

bendtorch-core@0.1.0.0 · src/tensor/contracts/replayed.bend:223

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/LAWS.bend as StorageLaws

223def value_after_read(+shape: Shape.Shape, +fill: F32, +ops: List<&2, StorageLaws.Op>, +read: U32, +index: U32) ->
224  {value(shape, fill, snoc(ops, StorageLaws.Read{read}), index) == value(shape, fill, ops, index) : F32}:
225  expected_snoc(ops, StorageLaws.Read{read}, U32.to_nat(Shape.count(shape)), index, fill)