TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tactic.Einops.Report.Analysis.ParseShape

Parse-shape reports #

This module reports the ordered axis bindings certified by parse_shape.

source
def TorchLean.Tensor.Internal.Report.Impl.decodeNameLength (expression : Lean.Expr) :
Lean.MetaM (Option (String × ℕ))

Decode one reflected (axis name, length) parse-shape binding.

Instances For
    source
    def TorchLean.Tensor.Internal.Report.Impl.decodeLocatedParseShapeAxis (expression : Lean.Expr) :
    Lean.MetaM (Option String)

    Decode one source axis retained by parse-shape ellipsis expansion.

    Instances For
      source
      def TorchLean.Tensor.Internal.Report.Impl.decodeExpandedParseShapeAxis (expression : Lean.Expr) :
      Lean.MetaM (Option String)

      Describe one parse-shape position after ellipsis expansion.

      Instances For
        source
        def TorchLean.Tensor.Internal.Report.Impl.formatBindings (bindings : List (String × ℕ)) :
        String

        Render parse-shape bindings in the public result order.

        Instances For
          source
          def TorchLean.Tensor.Internal.Report.Impl.concreteParseShapeReport (pattern inputShapeExpression : Lean.Expr) :
          Lean.MetaM (Option String)

          Decode the structural parse-shape check. The tensor scalar term is absent because this operation inspects only static shape metadata.

          Instances For