def zero_found

bendtorch-core@0.1.0.0 · src/tensor/slice_PROOF.bend:414

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/slice.bend as Slice

414# An element count of 0 has some dimension 0.
415def zero_found(+extent: U32, +rest: List<&2, U32>, e: {Shape.logical_numel(extent <> rest) == 0n : Nat},
416  rec: @e: {Shape.logical_numel(rest) == 0n : Nat} -> {Slice.holds_zero(rest) == True{} : Bool},
417  decision: Shape.BoolCase<Nat.is_eq(U32.to_nat(extent), 0n)>) -> {Slice.holds_zero(extent <> rest) == True{} : Bool}:
418  match decision:
419    case Shape.BTrue{equal}:
420      %equal : {Bool.or(_, Slice.holds_zero(rest)) == True{} : Bool}
421      {==}
422    case Shape.BFalse{+equal}:
423      %equal : {Bool.or(_, Slice.holds_zero(rest)) == True{} : Bool}
424      rec(mul_zero_factor(U32.to_nat(extent), Shape.logical_numel(rest), e, equal))