law write_outside

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

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

29law write_outside:
30  for +shape: Shape.Shape
31  for +fill: F32
32  for +index: U32
33  for +value: F32
34  for outside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == False{} : Bool}
35  Records.WriteOutside<shape, fill, index, value>