~/jendhub

def flat_numel

bendtorch@1.3.0.0 · tensor.bend:456

import bendtorch@1.3.0.0/tensor.bend as Tensor
import Base
import bend-ml-nat-lemmas@0.1.2.0/main.bend as NL

456# n * 1 == n, so a shape and its flattening hold the same count
457def flat_numel(+s: List<&2, Nat>) -> {numel(s) == numel([numel(s)]) : Nat}:
458  Equal.sym(Nat, Nat.mul(numel(s), 1n), numel(s), NL.mul_one_r(numel(s)))

Uses (6)

Used by (1)