def planned_shaped

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

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

482def planned_shaped(+dimensions: List<&2, U32>, +dim: U32, +start: U32, +stop: U32, +step: U32,
483  built: Shape.ConstructResult<Slice.resized(dimensions, U32.to_nat(dim), U32.from_nat(Slice.plan_length(Slice.plan_of(dimensions, dim, start, stop, step))))>) ->
484  Laws.PlannedAs(dimensions, dim, start, stop, step,
485    Slice.shaped(Slice.plan_of(dimensions, dim, start, stop, step),
486      Slice.resized(dimensions, U32.to_nat(dim), U32.from_nat(Slice.plan_length(Slice.plan_of(dimensions, dim, start, stop, step)))), built)):
487  match built:
488    case Shape.SError{error}:
489      Unit{}
490    case Shape.SBuilt{+shape, preserved}:
491      ({==}, preserved)