law read_outside

bendtorch-core@0.1.0.0 · src/tensor/read_write_contract_LAWS.bend:14

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/read_write_records.bend as Records

14law read_outside:
15  for +shape: Shape.Shape
16  for +fill: F32
17  for +index: U32
18  for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
19  Records.ReadContract<shape, fill, index, 8>