def built_success

bendtorch-core@0.1.0.0 · src/tensor/permute_build_proof.bend:533

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/tensor/layout.bend as Layout
import bendtorch-core@0.1.0.0/src/storage/main.bend as Storage
import bendtorch-core@0.1.0.0/src/tensor/core.bend as Core
import bendtorch-core@0.1.0.0/src/tensor/transforms.bend as Transforms
import bendtorch-core@0.1.0.0/src/tensor/transform_totality.bend as Totality

533def built_success(+input: Shape.Shape, +axes: List<&2, U32>, +plan: Layout.Plan<input, axes>, source: Core.Tensor<input>,
534  target: Core.Tensor<Layout.output(input, axes, plan)>) ->
535  Fact<{Totality.copy_succeeded(input, axes, plan, Transforms.built(input, axes, plan, source, target)) == True{} : Bool}>:
536  Core.TTensor{storage, exact} = target
537  match storage:
538    case Storage.Empty{}:
539      Fact{{==}}
540    case Storage.Owned{+d, +n, array, balanced, valid}:
541      owned_success(input, axes, plan, d, n, valid, exact, source)