def Std.Time.Day.Ordinal : Type

Ordinal represents a bounded value for days, which ranges between 1 and 31.

Equations

• Std.Time.Day.Ordinal = Std.Time.Internal.Bounded.LE 1 31

instance Std.Time.Day.instOrdinalRepr : Repr Std.Time.Day.Ordinal

instance Std.Time.Day.instOrdinalBEq : BEq Std.Time.Day.Ordinal

instance Std.Time.Day.instOrdinalLE : LE Std.Time.Day.Ordinal

instance Std.Time.Day.instOrdinalLT : LT Std.Time.Day.Ordinal

instance Std.Time.Day.instOfNatOrdinal {n : Nat} : OfNat Std.Time.Day.Ordinal n

Equations

• Std.Time.Day.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑30)) n)

instance Std.Time.Day.instDecidableLeOrdinal {x y : Std.Time.Day.Ordinal} : Decidable (x ≤ y)

Equations

• Std.Time.Day.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Day.instDecidableLtOrdinal {x y : Std.Time.Day.Ordinal} : Decidable (x < y)

instance Std.Time.Day.instInhabitedOrdinal : Inhabited Std.Time.Day.Ordinal

Equations

• Std.Time.Day.instInhabitedOrdinal = { default := 1 }

def Std.Time.Day.Offset : Type

Offset represents an offset in days. It is defined as an Int with a base unit of 86400 (the number of seconds in a day).

Equations

• Std.Time.Day.Offset = Std.Time.Internal.UnitVal 86400

instance Std.Time.Day.instOffsetRepr : Repr Std.Time.Day.Offset

Equations

• Std.Time.Day.instOffsetRepr = Std.Time.Internal.UnitVal.instRepr

instance Std.Time.Day.instOffsetBEq : BEq Std.Time.Day.Offset

instance Std.Time.Day.instOffsetInhabited : Inhabited Std.Time.Day.Offset

instance Std.Time.Day.instOffsetAdd : Add Std.Time.Day.Offset

instance Std.Time.Day.instOffsetSub : Sub Std.Time.Day.Offset

instance Std.Time.Day.instOffsetNeg : Neg Std.Time.Day.Offset

Equations

• Std.Time.Day.instOffsetNeg = Std.Time.Internal.UnitVal.instNeg

instance Std.Time.Day.instOffsetLE : LE Std.Time.Day.Offset

Equations

• Std.Time.Day.instOffsetLE = Std.Time.Internal.UnitVal.instLE

instance Std.Time.Day.instOffsetLT : LT Std.Time.Day.Offset

Equations

• Std.Time.Day.instOffsetLT = Std.Time.Internal.UnitVal.instLT

instance Std.Time.Day.instOffsetToString : ToString Std.Time.Day.Offset

instance Std.Time.Day.instOfNatOffset {n : Nat} : OfNat Std.Time.Day.Offset n

instance Std.Time.Day.instDecidableLeOffset {x y : Std.Time.Day.Offset} : Decidable (x ≤ y)

Equations

• Std.Time.Day.instDecidableLeOffset = inferInstanceAs (Decidable (x.val ≤ y.val))

instance Std.Time.Day.instDecidableLtOffset {x y : Std.Time.Day.Offset} : Decidable (x < y)

@[inline]

def Std.Time.Day.Ordinal.ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 31) : Std.Time.Day.Ordinal

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

def Std.Time.Day.Ordinal.OfYear (leap : Bool) : Type

OfYear represents the day ordinal within a year, which can be bounded between 1 and 365 or 366, depending on whether it's a leap year.

instance Std.Time.Day.Ordinal.instReprOfYear {leap : Bool} : Repr (Std.Time.Day.Ordinal.OfYear leap)

instance Std.Time.Day.Ordinal.instToStringOfYear {leap : Bool} : ToString (Std.Time.Day.Ordinal.OfYear leap)

@[inline]

def Std.Time.Day.Ordinal.OfYear.ofNat {leap : Bool} (data : Nat) (h : data ≥ 1 ∧ data ≤ if leap = true then 366 else 365 := by decide) : Std.Time.Day.Ordinal.OfYear leap

Creates an ordinal for a specific day within the year, ensuring that the provided day (data) is within the valid range for the year, which can be 1 to 365 or 366 for leap years.

Equations

• Std.Time.Day.Ordinal.OfYear.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat' data h

instance Std.Time.Day.Ordinal.instOfNatOfYear {leap : Bool} {n : Nat} : OfNat (Std.Time.Day.Ordinal.OfYear leap) n

Equations

• Std.Time.Day.Ordinal.instOfNatOfYear = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑365)) n)
• Std.Time.Day.Ordinal.instOfNatOfYear = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑364)) n)

instance Std.Time.Day.Ordinal.instInhabitedOfYear {leap : Bool} : Inhabited (Std.Time.Day.Ordinal.OfYear leap)

Equations

• Std.Time.Day.Ordinal.instInhabitedOfYear = { default := ⟨1, ⋯⟩ }

@[inline]

def Std.Time.Day.Ordinal.ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 31 := by decide) : Std.Time.Day.Ordinal

Creates an ordinal from a natural number, ensuring the number is within the valid range for days of a month (1 to 31).

Equations

• Std.Time.Day.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat' data h

@[inline]

def Std.Time.Day.Ordinal.ofFin (data : Fin 32) : Std.Time.Day.Ordinal

Creates an ordinal from a Fin value, ensuring it is within the valid range for days of the month (1 to 31). If the Fin value is 0, it is converted to 1.

@[inline]

def Std.Time.Day.Ordinal.toOffset (ordinal : Std.Time.Day.Ordinal) : Std.Time.Day.Offset

Converts an Ordinal to an Offset.

def Std.Time.Day.Ordinal.OfYear.toOffset {leap : Bool} (ofYear : Std.Time.Day.Ordinal.OfYear leap) : Std.Time.Day.Offset

Converts an OfYear ordinal to a Offset.

@[inline]

def Std.Time.Day.Offset.toOrdinal (off : Std.Time.Day.Offset) (h : off.val ≥ 1 ∧ off.val ≤ 31) : Std.Time.Day.Ordinal

Converts an Offset to an Ordinal.

Equations

• off.toOrdinal h = Std.Time.Internal.Bounded.LE.mk off.val h

@[inline]

def Std.Time.Day.Offset.ofNat (data : Nat) : Std.Time.Day.Offset

Creates an Offset from a natural number.

Equations

• Std.Time.Day.Offset.ofNat data = { val := ↑data }

@[inline]

def Std.Time.Day.Offset.ofInt (data : Int) : Std.Time.Day.Offset

Creates an Offset from an integer.

@[inline]

def Std.Time.Day.Offset.toNanoseconds (days : Std.Time.Day.Offset) : Std.Time.Nanosecond.Offset

Convert Day.Offset into Nanosecond.Offset.

@[inline]

def Std.Time.Day.Offset.ofNanoseconds (ns : Std.Time.Nanosecond.Offset) : Std.Time.Day.Offset

Convert Nanosecond.Offset into Day.Offset.

Equations

• Std.Time.Day.Offset.ofNanoseconds ns = Std.Time.Internal.UnitVal.ediv ns 86400000000000

@[inline]

def Std.Time.Day.Offset.toMilliseconds (days : Std.Time.Day.Offset) : Std.Time.Millisecond.Offset

Convert Day.Offset into Millisecond.Offset.

@[inline]

def Std.Time.Day.Offset.ofMilliseconds (ms : Std.Time.Millisecond.Offset) : Std.Time.Day.Offset

Convert Millisecond.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toSeconds (days : Std.Time.Day.Offset) : Std.Time.Second.Offset

Convert Day.Offset into Second.Offset.

Equations

• days.toSeconds = Std.Time.Internal.UnitVal.mul days 86400

@[inline]

def Std.Time.Day.Offset.ofSeconds (secs : Std.Time.Second.Offset) : Std.Time.Day.Offset

Convert Second.Offset into Day.Offset.

Equations

• Std.Time.Day.Offset.ofSeconds secs = Std.Time.Internal.UnitVal.ediv secs 86400

@[inline]

def Std.Time.Day.Offset.toMinutes (days : Std.Time.Day.Offset) : Std.Time.Minute.Offset

Convert Day.Offset into Minute.Offset.

@[inline]

def Std.Time.Day.Offset.ofMinutes (minutes : Std.Time.Minute.Offset) : Std.Time.Day.Offset

Convert Minute.Offset into Day.Offset.

@[inline]

def Std.Time.Day.Offset.toHours (days : Std.Time.Day.Offset) : Std.Time.Hour.Offset

Convert Day.Offset into Hour.Offset.

@[inline]

def Std.Time.Day.Offset.ofHours (hours : Std.Time.Hour.Offset) : Std.Time.Day.Offset

Convert Hour.Offset into Day.Offset.

Equations

• Std.Time.Day.Offset.ofHours hours = Std.Time.Internal.UnitVal.ediv hours 24