Documentation

Std.Time.Time.HourMarker

source
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.

Instances For
    source
    @[implicit_reducible]
    instance Std.Time.instReprHourMarker :
    Repr HourMarker
    source
    def Std.Time.instReprHourMarker.repr :
    HourMarker → Nat → Std.Format
    Instances For
      source
      @[implicit_reducible]
      instance Std.Time.instDecidableEqHourMarker :
      DecidableEq HourMarker
      source
      @[implicit_reducible]
      instance Std.Time.instOrdHourMarker :
      Ord HourMarker
      source
      instance Std.Time.instOrientedOrdHourMarker :
      OrientedOrd HourMarker
      source
      instance Std.Time.instTransOrdHourMarker :
      TransOrd HourMarker
      source
      instance Std.Time.instLawfulEqOrdHourMarker :
      LawfulEqOrd HourMarker
      source
      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.

      Instances For
        source
        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.

        Instances For
          source
          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.

          Instances For