source
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

Instances For

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

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

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

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

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

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

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

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

source
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)

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

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

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

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

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

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

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

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

source
instance Std.Time.Day.instTransOrdOrdinal :
TransOrd Ordinal
source
instance Std.Time.Day.instLawfulEqOrdOrdinal :
LawfulEqOrd Ordinal
source
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

Instances For

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

source
instance Std.Time.Day.instTransOrdOffset :
TransOrd Offset
source
instance Std.Time.Day.instLawfulEqOrdOffset :
LawfulEqOrd Offset
source
@[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

Instances For

source
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))

Instances For

source
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 }

source
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 }

source
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))))

source
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))))

source
instance Std.Time.Day.Ordinal.instTransOrdOfYear {leap : Bool} :
TransOrd (OfYear leap)
source
instance Std.Time.Day.Ordinal.instLawfulEqOrdOfYear {leap : Bool} :
LawfulEqOrd (OfYear leap)
source
@[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

Instances For

source
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)

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

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

source
@[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

Instances For

source
@[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✝

Instances For

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

Converts an `Ordinal` to an `Offset`.

Equations

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

Instances For

source
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 }

Instances For

source
@[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

Instances For

source
@[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 }

Instances For

source
@[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 }

Instances For

source
@[inline]
def Std.Time.Day.Offset.toNanoseconds (days : Offset) :
Nanosecond.Offset

Convert `Day.Offset` into `Nanosecond.Offset`.

Equations

- days.toNanoseconds = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.toNanoseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul days 86400000000000)

Instances For

source
@[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.cast Std.Time.Day.Offset.ofNanoseconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv ns 86400000000000)

Instances For

source
@[inline]
def Std.Time.Day.Offset.toMilliseconds (days : Offset) :
Millisecond.Offset

Convert `Day.Offset` into `Millisecond.Offset`.

Equations

- days.toMilliseconds = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.toMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.mul days 86400000)

Instances For

source
@[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.cast Std.Time.Day.Offset.ofMilliseconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv ms 86400000)

Instances For

source
@[inline]
def Std.Time.Day.Offset.toSeconds (days : Offset) :
Second.Offset

Convert `Day.Offset` into `Second.Offset`.

Equations

- days.toSeconds = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.toSeconds._proof_1✝ (Std.Time.Internal.UnitVal.mul days 86400)

Instances For

source
@[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.cast Std.Time.Day.Offset.ofSeconds._proof_1✝ (Std.Time.Internal.UnitVal.ediv secs 86400)

Instances For

source
@[inline]
def Std.Time.Day.Offset.toMinutes (days : Offset) :
Minute.Offset

Convert `Day.Offset` into `Minute.Offset`.

Equations

- days.toMinutes = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.toMinutes._proof_1✝ (Std.Time.Internal.UnitVal.mul days 1440)

Instances For

source
@[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.cast Std.Time.Day.Offset.ofMinutes._proof_1✝ (Std.Time.Internal.UnitVal.ediv minutes 1440)

Instances For

source
@[inline]
def Std.Time.Day.Offset.toHours (days : Offset) :
Hour.Offset

Convert `Day.Offset` into `Hour.Offset`.

Equations

- days.toHours = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.toHours._proof_1✝ (Std.Time.Internal.UnitVal.mul days 24)

Instances For

source
@[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.cast Std.Time.Day.Offset.ofHours._proof_1✝ (Std.Time.Internal.UnitVal.ediv hours 24)

Instances For