def holds_true

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

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

426def holds_true(+dimensions: List<&2, U32>, e: {Shape.logical_numel(dimensions) == 0n : Nat}) -> {Slice.holds_zero(dimensions) == True{} : Bool}:
427  match dimensions:
428    case Nil{}:
429      Empty.absurd({Slice.holds_zero(Nil{}) == True{} : Bool}, nat_clash(0n, e))
430    case +extent <> +rest:
431      zero_found(extent, rest, e, er => holds_true(rest, er), Shape.bool_case(Nat.is_eq(U32.to_nat(extent), 0n)))