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.

Built-in reductions retain their ordered scalar fold. mean, min, and max require nonempty fibers. Custom reducers instead consume a Multiset and may return a different scalar type; they do not expose a custom accumulation order.

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