def axis_extent_around

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

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

340def axis_extent_around(+prefix: List<&2, U32>, +extent: U32, +suffix: List<&2, U32>) ->
341  {Slice.axis_extent(List.append(&2, U32, prefix, extent <> suffix), Shape.rank_dimensions(prefix)) == U32.to_nat(extent) : Nat}:
342  match prefix:
343    case Nil{}:
344      {==}
345    case +head <> +tail:
346      axis_extent_around(tail, extent, suffix)