def sized_extent

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

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
import bendtorch-core@0.1.0.0/src/tensor/slice_LAWS.bend as Laws

348def sized_extent(+prefix: List<&2, U32>, +extent: U32, +suffix: List<&2, U32>, +empty: Bool) ->
349  {view_extent(Slice.sized(List.append(&2, U32, prefix, extent <> suffix), Shape.rank_dimensions(prefix), empty)) == U32.to_nat(extent) : Nat}:
350  match empty:
351    case True{}:
352      axis_extent_around(prefix, extent, suffix)
353    case False{}:
354      Equal.cong(Slice.View, Nat, v => view_extent(v),
355        Slice.view(List.append(&2, U32, prefix, extent <> suffix), Shape.rank_dimensions(prefix)),
356        Slice.View{Shape.logical_numel(prefix), U32.to_nat(extent), Shape.logical_numel(suffix)},
357        Laws.slice_view_around(prefix, extent, suffix))