law slice_plan_empty_view

bendtorch-core@0.1.0.0 · src/tensor/slice_LAWS.bend:171

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

171# An input with no element gets a plan with no view: neither build has a
172# cell then, so the plan forms no product of the other extents, which can
173# pass the largest Nat the runtime holds although no element exists.
174law slice_plan_empty_view:
175  for +dimensions: List<&2, U32>
176  for +dim: U32
177  for +start: U32
178  for +stop: U32
179  for +step: U32
180  for empty: {Shape.logical_numel(dimensions) == 0n : Nat}
181  {view_part(Slice.plan_of(dimensions, dim, start, stop, step)) == (0n, 0n) : Nat & Nat}