def planned_checked

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

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

493def planned_checked(+dimensions: List<&2, U32>, +dim: U32, +start: U32, +stop: U32, +step: U32, refused: Maybe<&2, Slice.Error>) ->
494  Laws.PlannedAs(dimensions, dim, start, stop, step, Slice.checked(dimensions, dim, start, stop, step, refused)):
495  match refused:
496    case Some{error}:
497      Unit{}
498    case None{}:
499      planned_shaped(dimensions, dim, start, stop, step,
500        Shape.construct(Slice.resized(dimensions, U32.to_nat(dim), U32.from_nat(Slice.plan_length(Slice.plan_of(dimensions, dim, start, stop, step))))))