TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Elab.Pack

Elaboration of pack and unpack #

This module implements heterogeneous-rank pack and unpack. It preserves symbolic component dimensions, verifies fixed-axis agreement, proves exact segment partitioning, and returns the dependent tensor family dictated by the checked metadata.

source
def TorchLean.Tensor.Internal.Elab.elabPack :
Lean.Elab.Term.TermElab

Elaborate a nonempty heterogeneous component family to verified packing, returning the packed tensor together with exact star-shape metadata.

Instances For
    source
    def TorchLean.Tensor.Internal.Elab.elabUnpack :
    Lean.Elab.Term.TermElab

    Elaborate unpack metadata, infer its optional -1 dimension, and return the heterogeneous component family certified by the reconstructed packed shape.

    Instances For