TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Elab.Transform

Elaboration of transformations and parse-shape expressions #

This module implements rearrange, expand, reduce, and parse_shape. Concrete dimensions use the executable checker for precise source diagnostics. Symbolic dimensions construct the same checked transformation type and prove every shape equation in the caller's Lean context.

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

Elaborate parse_shape, returning named symbolic dimensions only after the pattern's rank, literals, ellipsis, and wildcard obligations are proved.

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

    Elaborate rearrangement syntax to the coordinate equivalence certified by its symbolic or concrete transformation plan.

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

      Elaborate expand syntax to the generic pullback along its checked coordinate projection, including symbolic new-axis lengths.

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

        Elaborate built-in or user-supplied reduction syntax to the generic finite fiber reduction, proving nonemptiness for reducers without an empty case.

        Instances For