This module defines various units used for measuring, counting, and converting between days, months, years, weekdays, and weeks of the year.

The units are organized into types representing these time-related concepts, with operations provided to facilitate conversions and manipulations between them.

source
@[inline]
def Std.Time.Day.Offset.ofWeeks (week : Week.Offset) :
Offset

Convert `Week.Offset` into `Day.Offset`.

Equations

- Std.Time.Day.Offset.ofWeeks week = Std.Time.Internal.UnitVal.cast Std.Time.Day.Offset.ofWeeks._proof_1✝ (Std.Time.Internal.UnitVal.mul week 7)

Instances For

source
@[inline]
def Std.Time.Day.Offset.toWeeks (day : Offset) :
Week.Offset

Convert `Day.Offset` into `Week.Offset`.

Equations

- day.toWeeks = Std.Time.Internal.UnitVal.ediv day 7

Instances For