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 : HourMarker

  Ante meridiem.

• pm : HourMarker

  Post meridiem.

instance Std.Time.instReprHourMarker : Repr HourMarker

Equations

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

instance Std.Time.instBEqHourMarker : BEq HourMarker

Equations

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

def Std.Time.HourMarker.ofOrdinal (time : Hour.Ordinal) : 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 : HourMarker) (time : Internal.Bounded.LE 1 12) : 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 : Hour.Ordinal) : Internal.Bounded.LE 1 12 × 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.