source
def Std.Time.Nanosecond.Ordinal :
Type

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

Equations

- Std.Time.Nanosecond.Ordinal = Std.Time.Internal.Bounded.LE 0 999999999

Instances For

source
instance Std.Time.Nanosecond.instReprOrdinal :
Repr Ordinal
Equations

- Std.Time.Nanosecond.instReprOrdinal = Std.Time.Internal.Bounded.instRepr

source
instance Std.Time.Nanosecond.instDecidableEqOrdinal :
DecidableEq Ordinal
Equations

- Std.Time.Nanosecond.instDecidableEqOrdinal = Std.Time.Internal.Bounded.instDecidableEq

source
instance Std.Time.Nanosecond.instLEOrdinal :
LE Ordinal
Equations

- Std.Time.Nanosecond.instLEOrdinal = Std.Time.Internal.Bounded.instLE

source
instance Std.Time.Nanosecond.instLTOrdinal :
LT Ordinal
Equations

- Std.Time.Nanosecond.instLTOrdinal = Std.Time.Internal.Bounded.instLT

source
instance Std.Time.Nanosecond.instOfNatOrdinal {n : Nat} :
OfNat Ordinal n
Equations

- Std.Time.Nanosecond.instOfNatOrdinal = { ofNat := Std.Time.Internal.Bounded.LE.ofFin (Fin.ofNat (Nat.succ 999999999) n) }

source
instance Std.Time.Nanosecond.instInhabitedOrdinal :
Inhabited Ordinal
Equations

- Std.Time.Nanosecond.instInhabitedOrdinal = { default := 0 }

source
instance Std.Time.Nanosecond.instDecidableLeOrdinal {x y : Ordinal} :
Decidable (x ≤ y)
Equations

- Std.Time.Nanosecond.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Nanosecond.instDecidableLtOrdinal {x y : Ordinal} :
Decidable (x < y)
Equations

- Std.Time.Nanosecond.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

source
instance Std.Time.Nanosecond.instOrdOrdinal :
Ord Ordinal
Equations

- Std.Time.Nanosecond.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 0 999999999))

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.

Equations

- Std.Time.Nanosecond.Offset = Std.Time.Internal.UnitVal (1 / 1000000000)

Instances For

source
instance Std.Time.Nanosecond.instReprOffset :
Repr Offset
Equations

- Std.Time.Nanosecond.instReprOffset = Std.Time.Internal.UnitVal.instRepr

source
instance Std.Time.Nanosecond.instDecidableEqOffset :
DecidableEq Offset
Equations

- Std.Time.Nanosecond.instDecidableEqOffset = Std.Time.Internal.instDecidableEqUnitVal

source
instance Std.Time.Nanosecond.instInhabitedOffset :
Inhabited Offset
Equations

- Std.Time.Nanosecond.instInhabitedOffset = Std.Time.Internal.instInhabitedUnitVal

source
instance Std.Time.Nanosecond.instAddOffset :
Add Offset
Equations

- Std.Time.Nanosecond.instAddOffset = Std.Time.Internal.UnitVal.instAdd

source
instance Std.Time.Nanosecond.instSubOffset :
Sub Offset
Equations

- Std.Time.Nanosecond.instSubOffset = Std.Time.Internal.UnitVal.instSub

source
instance Std.Time.Nanosecond.instNegOffset :
Neg Offset
Equations

- Std.Time.Nanosecond.instNegOffset = Std.Time.Internal.UnitVal.instNeg

source
instance Std.Time.Nanosecond.instLEOffset :
LE Offset
Equations

- Std.Time.Nanosecond.instLEOffset = Std.Time.Internal.UnitVal.instLE

source
instance Std.Time.Nanosecond.instLTOffset :
LT Offset
Equations

- Std.Time.Nanosecond.instLTOffset = Std.Time.Internal.UnitVal.instLT

source
instance Std.Time.Nanosecond.instToStringOffset :
ToString Offset
Equations

- Std.Time.Nanosecond.instToStringOffset = Std.Time.Internal.UnitVal.instToString

source
instance Std.Time.Nanosecond.instDecidableLeOffset {x y : Offset} :
Decidable (x ≤ y)
Equations

- Std.Time.Nanosecond.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Nanosecond.instDecidableLtOffset {x y : Offset} :
Decidable (x < y)
Equations

- Std.Time.Nanosecond.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

source
instance Std.Time.Nanosecond.instOfNatOffset {n : Nat} :
OfNat Offset n
Equations

- Std.Time.Nanosecond.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }

source
instance Std.Time.Nanosecond.instOrdOffset :
Ord Offset
Equations

- Std.Time.Nanosecond.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal (1 / 1000000000)))

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.

Equations

- Std.Time.Nanosecond.Offset.ofNat data = { val := ↑data }

Instances For

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

Creates an `Offset` from an integer.

Equations

- Std.Time.Nanosecond.Offset.ofInt data = { val := data }

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.

Equations

- Std.Time.Nanosecond.Span = Std.Time.Internal.Bounded.LE (-999999999) 999999999

Instances For

source
instance Std.Time.Nanosecond.instReprSpan :
Repr Span
Equations

- Std.Time.Nanosecond.instReprSpan = Std.Time.Internal.Bounded.instRepr

source
instance Std.Time.Nanosecond.instDecidableEqSpan :
DecidableEq Span
Equations

- Std.Time.Nanosecond.instDecidableEqSpan = Std.Time.Internal.Bounded.instDecidableEq

source
instance Std.Time.Nanosecond.instLESpan :
LE Span
Equations

- Std.Time.Nanosecond.instLESpan = Std.Time.Internal.Bounded.instLE

source
instance Std.Time.Nanosecond.instLTSpan :
LT Span
Equations

- Std.Time.Nanosecond.instLTSpan = Std.Time.Internal.Bounded.instLT

source
instance Std.Time.Nanosecond.instInhabitedSpan :
Inhabited Span
Equations

- Std.Time.Nanosecond.instInhabitedSpan = { default := Std.Time.Internal.Bounded.LE.mk 0 Std.Time.Nanosecond.instInhabitedSpan._proof_1 }

source
instance Std.Time.Nanosecond.instDecidableLeSpan {x y : Span} :
Decidable (x ≤ y)
Equations

- Std.Time.Nanosecond.instDecidableLeSpan = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Nanosecond.instDecidableLtSpan {x y : Span} :
Decidable (x < y)
Equations

- Std.Time.Nanosecond.instDecidableLtSpan = inferInstanceAs (Decidable (x.val < y.val))

source
instance Std.Time.Nanosecond.instOrdSpan :
Ord Span
Equations

- Std.Time.Nanosecond.instOrdSpan = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE (-999999999) 999999999))

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`.

Equations

- span.toOffset = { val := span.val }

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.

Equations

- Std.Time.Nanosecond.Ordinal.OfDay = Std.Time.Internal.Bounded.LE 0 86400000000000

Instances For

source
instance Std.Time.Nanosecond.Ordinal.instReprOfDay :
Repr OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instReprOfDay = Std.Time.Internal.Bounded.instRepr

source
instance Std.Time.Nanosecond.Ordinal.instDecidableEqOfDay :
DecidableEq OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instDecidableEqOfDay = Std.Time.Internal.Bounded.instDecidableEq

source
instance Std.Time.Nanosecond.Ordinal.instLEOfDay :
LE OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instLEOfDay = Std.Time.Internal.Bounded.instLE

source
instance Std.Time.Nanosecond.Ordinal.instLTOfDay :
LT OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instLTOfDay = Std.Time.Internal.Bounded.instLT

source
instance Std.Time.Nanosecond.Ordinal.instInhabitedOfDay :
Inhabited OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instInhabitedOfDay = { default := Std.Time.Internal.Bounded.LE.mk 0 Std.Time.Nanosecond.Ordinal.instInhabitedOfDay._proof_1 }

source
instance Std.Time.Nanosecond.Ordinal.instDecidableLeOfDay {x y : OfDay} :
Decidable (x ≤ y)
Equations

- Std.Time.Nanosecond.Ordinal.instDecidableLeOfDay = inferInstanceAs (Decidable (x.val ≤ y.val))

source
instance Std.Time.Nanosecond.Ordinal.instDecidableLtOfDay {x y : OfDay} :
Decidable (x < y)
Equations

- Std.Time.Nanosecond.Ordinal.instDecidableLtOfDay = inferInstanceAs (Decidable (x.val < y.val))

source
instance Std.Time.Nanosecond.Ordinal.instOrdOfDay :
Ord OfDay
Equations

- Std.Time.Nanosecond.Ordinal.instOrdOfDay = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 0 86400000000000))

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.

Equations

- Std.Time.Nanosecond.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

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.

Equations

- Std.Time.Nanosecond.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat data h

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.

Equations

- Std.Time.Nanosecond.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin data

Instances For

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

Converts an `Ordinal` to an `Offset`.

Equations

- ordinal.toOffset = { val := ordinal.val }

Instances For