def numel_words_spec

bendtorch-core@0.1.0.0 · src/shape/core.bend:482

import bendtorch-core@0.1.0.0/src/shape/core.bend as Core

import Base

482def numel_words_spec(+dims: List<&2, U32>) -> {numel_words(dims) == numel(naturals(dims)) : Nat}:
483  match dims:
484    case Nil{}:
485      {==}
486    case +head <> +tail:
487      Equal.cong(Nat, Nat, value => Nat.mul(U32.to_nat(head), value), numel_words(tail), numel(naturals(tail)), numel_words_spec(tail))

Uses (9)

Used by (2)