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 an offset and a length, so malformed ranges cannot be represented.

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.

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

                The smallest span containing two spans that occur in source order.

                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
                    def TorchLean.Tensor.Internal.Syntax.instReprLocated.repr {α✝ : Type u_1} [Repr α✝] :
                    Located α✝ → Nat → Std.Format
                    Instances For
                      source
                      @[instance_reducible]
                      instance TorchLean.Tensor.Internal.Syntax.instReprLocated {α✝ : Type u_1} [Repr α✝] :
                      Repr (Located α✝)
                      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 α✝)
                        source
                        def TorchLean.Tensor.Internal.Syntax.Located.map {α : Type u} {β : Type v} (f : α → β) (value : Located α) :
                        Located β

                        Apply a function without changing a value's source location.

                        Instances For
                          source
                          @[simp]
                          theorem TorchLean.Tensor.Internal.Syntax.Located.map_value {α : Type u} {β : Type v} (f : α → β) (value : Located α) :
                          (map f value).value = f value.value

                          Mapping a located value applies the function to its payload.

                          source
                          @[simp]
                          theorem TorchLean.Tensor.Internal.Syntax.Located.map_span {α : Type u} {β : Type v} (f : α → β) (value : Located α) :
                          (map f value).span = value.span

                          Mapping a located value preserves its source span.