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.instReprHourMarker.repr }

def Std.Time.instReprHourMarker.repr : HourMarker → Nat → Std.Format

Equations

• Std.Time.instReprHourMarker.repr Std.Time.HourMarker.am prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.HourMarker.am")).group prec✝
• Std.Time.instReprHourMarker.repr Std.Time.HourMarker.pm prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Std.Time.HourMarker.pm")).group prec✝

instance Std.Time.instDecidableEqHourMarker : DecidableEq HourMarker

Equations

• Std.Time.instDecidableEqHourMarker x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Std.Time.instOrdHourMarker : Ord HourMarker

Equations

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

instance Std.Time.instOrientedOrdHourMarker : OrientedOrd HourMarker

instance Std.Time.instTransOrdHourMarker : TransOrd HourMarker

instance Std.Time.instLawfulEqOrdHourMarker : LawfulEqOrd HourMarker

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.