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 Ordinal

Equations

• Std.Time.Day.instOrdinalRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Day.instOrdinalDecidableEq : DecidableEq Ordinal

Equations

• Std.Time.Day.instOrdinalDecidableEq = Std.Time.Internal.Bounded.instDecidableEq

instance Std.Time.Day.instOrdinalLE : LE Ordinal

Equations

• Std.Time.Day.instOrdinalLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Day.instOrdinalLT : LT Ordinal

Equations

• Std.Time.Day.instOrdinalLT = Std.Time.Internal.Bounded.instLT

instance Std.Time.Day.instOfNatOrdinal {n : Nat} : OfNat 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 : Ordinal} : Decidable (x ≤ y)

Equations

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

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

Equations

• Std.Time.Day.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

instance Std.Time.Day.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

instance Std.Time.Day.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Day.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 31))

instance Std.Time.Day.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Day.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

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 Offset

Equations

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

instance Std.Time.Day.instOffsetDecidableEq : DecidableEq Offset

Equations

• Std.Time.Day.instOffsetDecidableEq = Std.Time.Internal.instDecidableEqUnitVal

instance Std.Time.Day.instOffsetInhabited : Inhabited Offset

Equations

• Std.Time.Day.instOffsetInhabited = Std.Time.Internal.instInhabitedUnitVal

instance Std.Time.Day.instOffsetAdd : Add Offset

Equations

• Std.Time.Day.instOffsetAdd = Std.Time.Internal.UnitVal.instAdd

instance Std.Time.Day.instOffsetSub : Sub Offset

Equations

• Std.Time.Day.instOffsetSub = Std.Time.Internal.UnitVal.instSub

instance Std.Time.Day.instOffsetNeg : Neg Offset

Equations

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

instance Std.Time.Day.instOffsetLE : LE Offset

Equations

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

instance Std.Time.Day.instOffsetLT : LT Offset

Equations

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

instance Std.Time.Day.instOffsetToString : ToString Offset

Equations

• Std.Time.Day.instOffsetToString = Std.Time.Internal.UnitVal.instToString

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

Equations

• Std.Time.Day.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat n }

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

Equations

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

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

Equations

• Std.Time.Day.instDecidableLtOffset = inferInstanceAs (Decidable (x.val < y.val))

instance Std.Time.Day.instOrdOffset : Ord Offset

Equations

• Std.Time.Day.instOrdOffset = inferInstanceAs (Ord (Std.Time.Internal.UnitVal 86400))

instance Std.Time.Day.instTransOrdOffset : TransOrd Offset

instance Std.Time.Day.instLawfulEqOrdOffset : LawfulEqOrd Offset

@[inline]

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

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

Equations

• Std.Time.Day.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

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.

Equations

• Std.Time.Day.Ordinal.OfYear leap = Std.Time.Internal.Bounded.LE 1 (Int.ofNat (if leap = true then 366 else 365))

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

Equations

• Std.Time.Day.Ordinal.instReprOfYear = { reprPrec := fun (r : Std.Time.Day.Ordinal.OfYear leap) (p : Nat) => reprPrec r.val p }

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

Equations

• Std.Time.Day.Ordinal.instToStringOfYear = { toString := fun (r : Std.Time.Day.Ordinal.OfYear leap) => toString r.val }

instance Std.Time.Day.Ordinal.instDecidableEqOfYear {leap : Bool} : DecidableEq (OfYear leap)

Equations

• Std.Time.Day.Ordinal.instDecidableEqOfYear = inferInstanceAs (DecidableEq (Std.Time.Internal.Bounded.LE 1 (Int.ofNat (if leap = true then 366 else 365))))

instance Std.Time.Day.Ordinal.instOrdOfYear {leap : Bool} : Ord (OfYear leap)

Equations

• Std.Time.Day.Ordinal.instOrdOfYear = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 (Int.ofNat (if leap = true then 366 else 365))))

instance Std.Time.Day.Ordinal.instTransOrdOfYear {leap : Bool} : TransOrd (OfYear leap)

instance Std.Time.Day.Ordinal.instLawfulEqOrdOfYear {leap : Bool} : LawfulEqOrd (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) : 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 (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 (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) : 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) : 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.

Equations

• Std.Time.Day.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin' data Std.Time.Day.Ordinal.ofFin._proof_1

@[inline]

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

Converts an Ordinal to an Offset.

Equations

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

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

Converts an OfYear ordinal to a Offset.

Equations

• ofYear.toOffset = { val := ofYear.val }

@[inline]

def Std.Time.Day.Offset.toOrdinal (off : Offset) (h : off.val ≥ 1 ∧ off.val ≤ 31) : 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) : 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) : Offset

Creates an Offset from an integer.

Equations

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

@[inline]

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

Convert Day.Offset into Nanosecond.Offset.

Equations

• days.toNanoseconds = Std.Time.Internal.UnitVal.mul days 86400000000000

@[inline]

def Std.Time.Day.Offset.ofNanoseconds (ns : Nanosecond.Offset) : 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 : Offset) : Millisecond.Offset

Convert Day.Offset into Millisecond.Offset.

Equations

• days.toMilliseconds = Std.Time.Internal.UnitVal.mul days 86400000

@[inline]

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

Convert Millisecond.Offset into Day.Offset.

Equations

• Std.Time.Day.Offset.ofMilliseconds ms = Std.Time.Internal.UnitVal.ediv ms 86400000

@[inline]

def Std.Time.Day.Offset.toSeconds (days : Offset) : 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 : Second.Offset) : 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 : Offset) : Minute.Offset

Convert Day.Offset into Minute.Offset.

Equations

• days.toMinutes = Std.Time.Internal.UnitVal.mul days 1440

@[inline]

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

Convert Minute.Offset into Day.Offset.

Equations

• Std.Time.Day.Offset.ofMinutes minutes = Std.Time.Internal.UnitVal.ediv minutes 1440

@[inline]

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

Convert Day.Offset into Hour.Offset.

Equations

• days.toHours = Std.Time.Internal.UnitVal.mul days 24

@[inline]

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

Convert Hour.Offset into Day.Offset.

Equations

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