TorchLean API

Docs HomeGuideExamplesGraphs

Std.Time.Time.Unit.Nanosecond

source
def Std.Time.Nanosecond.Ordinal :
Type

Ordinal represents a nanosecond value that is bounded between 0 and 999,999,999 nanoseconds.

Instances For
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instReprOrdinal :
    Repr Ordinal
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instDecidableEqOrdinal :
    DecidableEq Ordinal
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instLEOrdinal :
    LE Ordinal
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instLTOrdinal :
    LT Ordinal
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instOfNatOrdinal {n : Nat} :
    OfNat Ordinal n
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instInhabitedOrdinal :
    Inhabited Ordinal
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instDecidableLeOrdinal {x y : Ordinal} :
    Decidable (x ≤ y)
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instDecidableLtOrdinal {x y : Ordinal} :
    Decidable (x < y)
    source
    @[implicit_reducible]
    instance Std.Time.Nanosecond.instOrdOrdinal :
    Ord Ordinal
    source
    instance Std.Time.Nanosecond.instTransOrdOrdinal :
    TransOrd Ordinal
    source
    instance Std.Time.Nanosecond.instLawfulEqOrdOrdinal :
    LawfulEqOrd Ordinal
    source
    def Std.Time.Nanosecond.Offset :
    Type

    Offset represents a time offset in nanoseconds.

    Instances For
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instReprOffset :
      Repr Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instDecidableEqOffset :
      DecidableEq Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instInhabitedOffset :
      Inhabited Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instAddOffset :
      Add Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instSubOffset :
      Sub Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instNegOffset :
      Neg Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instLEOffset :
      LE Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instLTOffset :
      LT Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instToStringOffset :
      ToString Offset
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instDecidableLeOffset {x y : Offset} :
      Decidable (x ≤ y)
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instDecidableLtOffset {x y : Offset} :
      Decidable (x < y)
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instOfNatOffset {n : Nat} :
      OfNat Offset n
      source
      @[implicit_reducible]
      instance Std.Time.Nanosecond.instOrdOffset :
      Ord Offset
      source
      instance Std.Time.Nanosecond.instTransOrdOffset :
      TransOrd Offset
      source
      instance Std.Time.Nanosecond.instLawfulEqOrdOffset :
      LawfulEqOrd Offset
      source
      @[inline]
      def Std.Time.Nanosecond.Offset.ofNat (data : Nat) :
      Offset

      Creates an Offset from a natural number.

      Instances For
        source
        @[inline]
        def Std.Time.Nanosecond.Offset.ofInt (data : Int) :
        Offset

        Creates an Offset from an integer.

        Instances For
          source
          def Std.Time.Nanosecond.Span :
          Type

          Span represents a bounded value for nanoseconds, ranging between -999999999 and 999999999. This can be used for operations that involve differences or adjustments within this range.

          Instances For
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instReprSpan :
            Repr Span
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instDecidableEqSpan :
            DecidableEq Span
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instLESpan :
            LE Span
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instLTSpan :
            LT Span
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instInhabitedSpan :
            Inhabited Span
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instDecidableLeSpan {x y : Span} :
            Decidable (x ≤ y)
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instDecidableLtSpan {x y : Span} :
            Decidable (x < y)
            source
            @[implicit_reducible]
            instance Std.Time.Nanosecond.instOrdSpan :
            Ord Span
            source
            instance Std.Time.Nanosecond.instTransOrdSpan :
            TransOrd Span
            source
            instance Std.Time.Nanosecond.instLawfulEqOrdSpan :
            LawfulEqOrd Span
            source
            def Std.Time.Nanosecond.Span.toOffset (span : Span) :
            Offset

            Creates a new Offset out of a Span.

            Instances For
              source
              def Std.Time.Nanosecond.Ordinal.OfDay :
              Type

              Ordinal represents a bounded value for nanoseconds in a day, which ranges between 0 and 86400000000000.

              Instances For
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instReprOfDay :
                Repr OfDay
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instDecidableEqOfDay :
                DecidableEq OfDay
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instLEOfDay :
                LE OfDay
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instLTOfDay :
                LT OfDay
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instInhabitedOfDay :
                Inhabited OfDay
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instDecidableLeOfDay {x y : OfDay} :
                Decidable (x ≤ y)
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instDecidableLtOfDay {x y : OfDay} :
                Decidable (x < y)
                source
                @[implicit_reducible]
                instance Std.Time.Nanosecond.Ordinal.instOrdOfDay :
                Ord OfDay
                source
                instance Std.Time.Nanosecond.Ordinal.instTransOrdOfDay :
                TransOrd OfDay
                source
                instance Std.Time.Nanosecond.Ordinal.instLawfulEqOrdOfDay :
                LawfulEqOrd OfDay
                source
                @[inline]
                def Std.Time.Nanosecond.Ordinal.ofInt (data : Int) (h : 0 ≤ data ∧ data ≤ 999999999) :
                Ordinal

                Creates an Ordinal from an integer, ensuring the value is within bounds.

                Instances For
                  source
                  @[inline]
                  def Std.Time.Nanosecond.Ordinal.ofNat (data : Nat) (h : data ≤ 999999999) :
                  Ordinal

                  Creates an Ordinal from a natural number, ensuring the value is within bounds.

                  Instances For
                    source
                    @[inline]
                    def Std.Time.Nanosecond.Ordinal.ofFin (data : Fin 1000000000) :
                    Ordinal

                    Creates an Ordinal from a Fin, ensuring the value is within bounds.

                    Instances For
                      source
                      @[inline]
                      def Std.Time.Nanosecond.Ordinal.toOffset (ordinal : Ordinal) :
                      Offset

                      Converts an Ordinal to an Offset.

                      Instances For