Documentation

Std.Time.Date.Unit.Day

def Std.Time.Day.Ordinal :

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

instance Std.Time.Day.instOrdinalRepr :

Repr Std.Time.Day.Ordinal

Equations

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

instance Std.Time.Day.instOrdinalBEq :

BEq Std.Time.Day.Ordinal

Equations

Std.Time.Day.instOrdinalBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Day.instOrdinalLE :

LE Std.Time.Day.Ordinal

Equations

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

instance Std.Time.Day.instOrdinalLT :

LT Std.Time.Day.Ordinal

Equations

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

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)

Equations

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

instance Std.Time.Day.instInhabitedOrdinal :

Inhabited Std.Time.Day.Ordinal

Equations

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

def Std.Time.Day.Offset :

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

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

Equations

Std.Time.Day.instOffsetBEq = Std.Time.Internal.instBEqUnitVal

instance Std.Time.Day.instOffsetInhabited :

Inhabited Std.Time.Day.Offset

Equations

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

instance Std.Time.Day.instOffsetAdd :

Add Std.Time.Day.Offset

Equations

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

instance Std.Time.Day.instOffsetSub :

Sub Std.Time.Day.Offset

Equations

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

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

Equations

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

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

OfNat Std.Time.Day.Offset n

Equations

Std.Time.Day.instOfNatOffset = { ofNat := Std.Time.Internal.UnitVal.ofNat 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)

Equations

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

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

Equations

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

Instances For

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

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

instance Std.Time.Day.Ordinal.instReprOfYear {leap : Bool} :

Repr (Std.Time.Day.Ordinal.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 (Std.Time.Day.Ordinal.OfYear leap)

Equations

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

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

Instances For

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

Instances For

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

Equations

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

Instances For

@[inline]

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

Std.Time.Day.Offset

Converts an Ordinal to an Offset.

Equations

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

Instances For

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.

Equations

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

Instances For

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

Instances For

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

Instances For

@[inline]

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

Std.Time.Day.Offset

Creates an Offset from an integer.

Equations

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

Instances For

@[inline]

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

Std.Time.Nanosecond.Offset

Convert Day.Offset into Nanosecond.Offset.

Equations

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

Instances For

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

Instances For

@[inline]

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

Std.Time.Millisecond.Offset

Convert Day.Offset into Millisecond.Offset.

Equations

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

Instances For

@[inline]

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

Std.Time.Day.Offset

Convert Millisecond.Offset into Day.Offset.

Equations

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

Instances For

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

Instances For

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

Instances For

@[inline]

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

Std.Time.Minute.Offset

Convert Day.Offset into Minute.Offset.

Equations

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

Instances For

@[inline]

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

Std.Time.Day.Offset

Convert Minute.Offset into Day.Offset.

Equations

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

Instances For

@[inline]

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

Std.Time.Hour.Offset

Convert Day.Offset into Hour.Offset.

Equations

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

Instances For

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

Instances For