TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

NN.Tensor.Internal.Syntax.Span

Source locations #

TorchLean.Tensor.Internal records source locations as half-open ranges measured in Unicode scalar values. A span stores a natural-number offset and length, so its endpoint cannot precede its start. The type does not certify bounds within a particular source string.

source
structure TorchLean.Tensor.Internal.Syntax.Span :
Type

A half-open source range, measured in Unicode scalar values.

  • offset : Nat

    Number of Unicode scalar values preceding the range.

  • length : Nat

    Number of Unicode scalar values contained in the range.

Instances For
    source
    def TorchLean.Tensor.Internal.Syntax.instReprSpan.repr :
    Span → Nat → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance TorchLean.Tensor.Internal.Syntax.instReprSpan :
      Repr Span
      source
      def TorchLean.Tensor.Internal.Syntax.instDecidableEqSpan.decEq (x✝ x✝¹ : Span) :
      Decidable (x✝ = x✝¹)
      Instances For
        source
        @[instance_reducible]
        instance TorchLean.Tensor.Internal.Syntax.instDecidableEqSpan :
        DecidableEq Span
        source
        @[instance_reducible]
        instance TorchLean.Tensor.Internal.Syntax.instBEqSpan :
        BEq Span
        source
        def TorchLean.Tensor.Internal.Syntax.instBEqSpan.beq :
        Span → Span → Bool
        Instances For
          source
          def TorchLean.Tensor.Internal.Syntax.Span.stop (span : Span) :
          Nat

          The first offset after a source span.

          Instances For
            source
            def TorchLean.Tensor.Internal.Syntax.Span.point (offset : Nat) :
            Span

            The empty span at offset.

            Instances For
              source
              def TorchLean.Tensor.Internal.Syntax.Span.between (start stop : Nat) :
              Span

              The half-open range from start to stop, empty at start when stop < start.

              Instances For
                source
                def TorchLean.Tensor.Internal.Syntax.Span.join (left right : Span) :
                Span

                The range from left.offset to right.stop.

                This is the smallest containing span when left.offset ≤ right.offset and left.stop ≤ right.stop, as for the ordered delimiters supplied by the parsers.

                Instances For
                  source
                  @[simp]
                  theorem TorchLean.Tensor.Internal.Syntax.Span.stop_mk (offset length : Nat) :
                  { offset := offset, length := length }.stop = offset + length

                  The endpoint of an explicitly constructed span is offset plus length.

                  source
                  @[simp]
                  theorem TorchLean.Tensor.Internal.Syntax.Span.stop_point (offset : Nat) :
                  (point offset).stop = offset

                  A point span ends at its starting offset.

                  source
                  theorem TorchLean.Tensor.Internal.Syntax.Span.offset_le_stop (span : Span) :
                  span.offset ≤ span.stop

                  The start of a span never lies after its endpoint.

                  source
                  structure TorchLean.Tensor.Internal.Syntax.Located (α : Type u) :
                  Type u

                  A value together with its location in source text.

                  • value : α

                    Parsed value.

                  • span : Span

                    Source range from which the value was parsed.

                  Instances For
                    source
                    @[instance_reducible]
                    instance TorchLean.Tensor.Internal.Syntax.instReprLocated {α✝ : Type u_1} [Repr α✝] :
                    Repr (Located α✝)
                    source
                    def TorchLean.Tensor.Internal.Syntax.instReprLocated.repr {α✝ : Type u_1} [Repr α✝] :
                    Located α✝ → Nat → Std.Format
                    Instances For
                      source
                      def TorchLean.Tensor.Internal.Syntax.instDecidableEqLocated.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Located α✝) :
                      Decidable (x✝ = x✝¹)
                      Instances For
                        source
                        @[instance_reducible]
                        instance TorchLean.Tensor.Internal.Syntax.instDecidableEqLocated {α✝ : Type u_1} [DecidableEq α✝] :
                        DecidableEq (Located α✝)