1 import Base 2 import ../shape/core.bend as Shape 3 import ./clone_metadata_records.bend as Records 4 5 law clone_contract: 6 for +shape: Shape.Shape 7 for +fill: F32 8 Records.CloneContract 9 10 law clone_write: 11 for +shape: Shape.Shape 12 for +fill: F32 13 for +index: U32 14 for +value: F32 15 for inside: {Nat.is_lt(U32.to_nat(index), Shape.logical_numel(Shape.dimensions(shape))) == True{} : Bool} 16 Records.CloneWrite 17 18 law metadata_contract: 19 for +shape: Shape.Shape 20 for +fill: F32 21 Records.MetadataContract