def supplied_count
bendtorch-core@0.1.0.0 · src/tensor/construction_PROOF.bend:383
import bendtorch-core@0.1.0.0/src/tensor/construction_PROOF.bend as ConstructionPROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/lifecycle.bend as Lifecycle
383def supplied_count(+shape: Shape.Shape, +values: List<&2, F32>,
384 decided: {True{} == Nat.is_eq(List.length(&2, F32, values), Shape.elements(shape)) : Bool}) ->
385 {Shape.logical_numel(Shape.dimensions(shape)) == List.length(&2, F32, values) : Nat}:
386 Equal.trans(Nat, Shape.logical_numel(Shape.dimensions(shape)), Shape.elements(shape), List.length(&2, F32, values),
387 Equal.sym(Nat, Shape.elements(shape), Shape.logical_numel(Shape.dimensions(shape)), Shape.elements_exact(shape)),
388 Equal.sym(Nat, List.length(&2, F32, values), Shape.elements(shape),
389 Lifecycle.natural_equal(List.length(&2, F32, values), Shape.elements(shape), decided)))