def zero_numel
bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:391
import bendtorch-core@0.1.0.0/src/tensor/slice_PROOF.bend as SlicePROOF
import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice
391def zero_numel(+dimensions: List<&2, U32>, h: {Slice.holds_zero(dimensions) == True{} : Bool}) ->
392 {Shape.logical_numel(dimensions) == 0n : Nat}:
393 match dimensions:
394 case Nil{}:
395 Empty.absurd({Shape.logical_numel(Nil{}) == 0n : Nat}, Arith.clash(h))
396 case +extent <> +rest:
397 zero_head(extent, rest, h, hr => zero_numel(rest, hr), Shape.bool_case(Nat.is_eq(U32.to_nat(extent), 0n)))