inductive Std.Time.HourMarker : Type

HourMarker represents the two 12-hour periods of the day: am for hours between 12:00 AM and 11:59 AM, and pm for hours between 12:00 PM and 11:59 PM.

• am : Std.Time.HourMarker

  Ante meridiem.

• pm : Std.Time.HourMarker

  Post meridiem.

instance Std.Time.instReprHourMarker : Repr Std.Time.HourMarker

Equations

• Std.Time.instReprHourMarker = { reprPrec := Std.Time.reprHourMarker✝ }

instance Std.Time.instBEqHourMarker : BEq Std.Time.HourMarker

Equations

• Std.Time.instBEqHourMarker = { beq := Std.Time.beqHourMarker✝ }

def Std.Time.HourMarker.ofOrdinal (time : Std.Time.Hour.Ordinal) : Std.Time.HourMarker

ofOrdinal converts an Hour.Ordinal value to an HourMarker, indicating whether it is AM or PM.

Equations

• Std.Time.HourMarker.ofOrdinal time = if time.val ≥ 12 then Std.Time.HourMarker.pm else Std.Time.HourMarker.am

def Std.Time.HourMarker.toAbsolute (marker : Std.Time.HourMarker) (time : Std.Time.Internal.Bounded.LE 1 12) : Std.Time.Hour.Ordinal

Converts a 12-hour clock time to a 24-hour clock time based on the HourMarker.

Equations

• Std.Time.HourMarker.am.toAbsolute time = if time.val = 12 then 0 else time.expand Std.Time.HourMarker.toAbsolute.proof_1 Std.Time.HourMarker.toAbsolute.proof_2
• Std.Time.HourMarker.pm.toAbsolute time = if time.val = 12 then 12 else (time.add 12).emod 24 Std.Time.HourMarker.toAbsolute.proof_3

def Std.Time.HourMarker.toRelative (hour : Std.Time.Hour.Ordinal) : Std.Time.Internal.Bounded.LE 1 12 × Std.Time.HourMarker

Converts a 24-hour clock time to a 12-hour clock time with a HourMarker.

Equations

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