def Actus.Util.Date.isLeapYear (y : Nat) : Bool

Proleptic-Gregorian leap-year test.

Equations

• Actus.Util.Date.isLeapYear y = (y % 4 == 0 && y % 100 != 0 || y % 400 == 0)

def Actus.Util.Date.daysInMonth (y m : Nat) : Nat

Number of days in month m (1–12) of year y.

Equations

• Actus.Util.Date.daysInMonth y 1 = 31
• Actus.Util.Date.daysInMonth y 2 = if Actus.Util.Date.isLeapYear y = true then 29 else 28
• Actus.Util.Date.daysInMonth y 3 = 31
• Actus.Util.Date.daysInMonth y 4 = 30
• Actus.Util.Date.daysInMonth y 5 = 31
• Actus.Util.Date.daysInMonth y 6 = 30
• Actus.Util.Date.daysInMonth y 7 = 31
• Actus.Util.Date.daysInMonth y 8 = 31
• Actus.Util.Date.daysInMonth y 9 = 30
• Actus.Util.Date.daysInMonth y 10 = 31
• Actus.Util.Date.daysInMonth y 11 = 30
• Actus.Util.Date.daysInMonth y 12 = 31
• Actus.Util.Date.daysInMonth y m = 30

def Actus.Util.Date.toEpochDay (d : Protocol.LocalTime) : Int

Days from 1970-01-01 (negative for earlier dates).

Equations

• One or more equations did not get rendered due to their size.

def Actus.Util.Date.ofEpochDay (z : Int) : Protocol.LocalTime

Inverse of toEpochDay (Hinnant civil_from_days).

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Actus.Util.Date.instOrdLocalTime : Ord Protocol.LocalTime

Equations

• Actus.Util.Date.instOrdLocalTime = { compare := fun (a b : Actus.Protocol.LocalTime) => compare (Actus.Util.Date.toEpochDay a) (Actus.Util.Date.toEpochDay b) }

@[implicit_reducible]

instance Actus.Util.Date.instLELocalTime : LE Protocol.LocalTime

Equations

• Actus.Util.Date.instLELocalTime = { le := fun (a b : Actus.Protocol.LocalTime) => Actus.Util.Date.toEpochDay a ≤ Actus.Util.Date.toEpochDay b }

@[implicit_reducible]

instance Actus.Util.Date.instLTLocalTime : LT Protocol.LocalTime

Equations

• Actus.Util.Date.instLTLocalTime = { lt := fun (a b : Actus.Protocol.LocalTime) => Actus.Util.Date.toEpochDay a < Actus.Util.Date.toEpochDay b }

@[implicit_reducible]

instance Actus.Util.Date.instBEqLocalTime : BEq Protocol.LocalTime

Equations

• Actus.Util.Date.instBEqLocalTime = { beq := fun (a b : Actus.Protocol.LocalTime) => Actus.Util.Date.toEpochDay a == Actus.Util.Date.toEpochDay b }

def Actus.Util.Date.weekday (d : Protocol.LocalTime) : Nat

Weekday, 0 = Sunday … 6 = Saturday (Hinnant weekday_from_days).

Equations

• Actus.Util.Date.weekday d = (if Actus.Util.Date.toEpochDay d ≥ -4 then (Actus.Util.Date.toEpochDay d + 4) % 7 else (Actus.Util.Date.toEpochDay d + 5) % 7 + 6).toNat

def Actus.Util.Date.addMonths (d : Protocol.LocalTime) (n : Nat) : Protocol.LocalTime

Add n whole months, clamping the day to the target month's length.

Equations

• One or more equations did not get rendered due to their size.

def Actus.Util.Date.addDays (d : Protocol.LocalTime) (n : Nat) : Protocol.LocalTime

Add n whole days.

Equations

• Actus.Util.Date.addDays d n = Actus.Util.Date.ofEpochDay (Actus.Util.Date.toEpochDay d + ↑n)

def Actus.Util.Date.monthsOfUnit : String → Option Nat

Number of months in one ACTUS period unit (Q=3, H=6, Y=12, M=1).

Equations

• Actus.Util.Date.monthsOfUnit "M" = some 1
• Actus.Util.Date.monthsOfUnit "Q" = some 3
• Actus.Util.Date.monthsOfUnit "H" = some 6
• Actus.Util.Date.monthsOfUnit "Y" = some 12
• Actus.Util.Date.monthsOfUnit x✝ = none

def Actus.Util.Date.daysOfUnit : String → Option Nat

Number of days in one ACTUS period unit (D=1, W=7).

Equations

• Actus.Util.Date.daysOfUnit "D" = some 1
• Actus.Util.Date.daysOfUnit "W" = some 7
• Actus.Util.Date.daysOfUnit x✝ = none

def Actus.Util.Date.addPeriod (d : Protocol.LocalTime) (n : Nat) (unit : String) : Protocol.LocalTime

Advance d by n units of the given period (D/W/M/Q/H/Y).

Equations

• One or more equations did not get rendered due to their size.

def Actus.Util.Date.addCycle (d : Protocol.LocalTime) (c : Protocol.Cycle) : Protocol.LocalTime

Advance d by one Cycle.

Equations

• Actus.Util.Date.addCycle d c = Actus.Util.Date.addPeriod d c.n c.period

def Actus.Util.Date.subMonths (d : Protocol.LocalTime) (n : Nat) : Protocol.LocalTime

Subtract n whole months (floor division on the month index).

Equations

• One or more equations did not get rendered due to their size.

def Actus.Util.Date.subPeriod (d : Protocol.LocalTime) (n : Nat) (unit : String) : Protocol.LocalTime

Move d back by n units of the given period (D/W/M/Q/H/Y).

Equations

• One or more equations did not get rendered due to their size.