def created_exact

bendtorch-core@0.1.0.0 · src/tensor/read_contract.bend:39

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
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle

39def created_exact(+shape: Shape.Shape, +fill: F32) -> {Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)) == Shape.logical_numel(Shape.dimensions(shape)) : Nat}:
40  Equal.trans(Nat, Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Shape.logical_numel(Shape.dimensions(shape)),
41    Equal.sym(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), Lifecycle.logical_length(StorageLaws.created(Shape.count(shape), fill)), size_is_length(StorageLaws.created(Shape.count(shape), fill))),
42    Equal.trans(Nat, StorageLaws.size(StorageLaws.created(Shape.count(shape), fill)), U32.to_nat(Shape.count(shape)), Shape.logical_numel(Shape.dimensions(shape)), created_size(shape, fill), count_exact(shape)))