TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Syntax.Diagnostic

Parser diagnostics #

Diagnostics carry a stable machine-readable code, a human-readable message, and the smallest useful source span.

source
inductive TorchLean.Tensor.Internal.Syntax.DiagnosticCode :
Type

Stable categories for syntax errors.

  • unknownCharacter : DiagnosticCode

    The lexer encountered a character outside the einops token alphabet.

  • missingArrow : DiagnosticCode

    A pattern that requires -> did not contain one.

  • duplicateArrow : DiagnosticCode

    A pattern contained more than one ->.

  • unexpectedToken : DiagnosticCode

    A token was not valid at its position in the current grammar.

  • unbalancedParenthesis : DiagnosticCode

    An opening or closing parenthesis had no matching partner.

  • nestedParenthesis : DiagnosticCode

    A parenthesized axis group contained another parenthesized group.

  • invalidIdentifier : DiagnosticCode

    A word did not satisfy the selected identifier policy.

  • duplicateAxis : DiagnosticCode

    A named axis occurred more than once where uniqueness is required.

  • invalidAnonymousAxis : DiagnosticCode

    A numeric axis was zero or could not be decoded as a natural number.

  • duplicateEllipsis : DiagnosticCode

    An expression contained more than one ellipsis.

  • missingPackAxis : DiagnosticCode

    A pack pattern did not contain its required * axis.

  • duplicatePackAxis : DiagnosticCode

    A pack pattern contained more than one * axis.

Instances For
    source
    def TorchLean.Tensor.Internal.Syntax.instReprDiagnosticCode.repr :
    DiagnosticCode → Nat → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance TorchLean.Tensor.Internal.Syntax.instReprDiagnosticCode :
      Repr DiagnosticCode
      source
      @[instance_reducible]
      instance TorchLean.Tensor.Internal.Syntax.instDecidableEqDiagnosticCode :
      DecidableEq DiagnosticCode
      source
      @[instance_reducible]
      instance TorchLean.Tensor.Internal.Syntax.instBEqDiagnosticCode :
      BEq DiagnosticCode
      source
      def TorchLean.Tensor.Internal.Syntax.instBEqDiagnosticCode.beq :
      DiagnosticCode → DiagnosticCode → Bool
      Instances For
        source
        structure TorchLean.Tensor.Internal.Syntax.Diagnostic :
        Type

        A structured syntax error.

        • code : DiagnosticCode

          Stable machine-readable category of the parse failure.

        • message : String

          Human-readable explanation of the malformed pattern.

        • span : Span

          Smallest useful source range responsible for the failure.

        Instances For
          source
          def TorchLean.Tensor.Internal.Syntax.instReprDiagnostic.repr :
          Diagnostic → Nat → Std.Format
          Instances For
            source
            @[instance_reducible]
            instance TorchLean.Tensor.Internal.Syntax.instReprDiagnostic :
            Repr Diagnostic
            source
            @[instance_reducible]
            instance TorchLean.Tensor.Internal.Syntax.instDecidableEqDiagnostic :
            DecidableEq Diagnostic
            source
            def TorchLean.Tensor.Internal.Syntax.instDecidableEqDiagnostic.decEq (x✝ x✝¹ : Diagnostic) :
            Decidable (x✝ = x✝¹)
            Instances For
              source
              @[reducible, inline]
              abbrev TorchLean.Tensor.Internal.Syntax.Result (α : Type u) :
              Type u

              The result type used by the syntax front end.

              Instances For