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
    instance Std.Time.instReprHourMarker :
    Repr HourMarker
    Equations
      source
      instance Std.Time.instDecidableEqHourMarker :
      DecidableEq HourMarker
      Equations
        source
        instance Std.Time.instOrdHourMarker :
        Ord HourMarker
        Equations
          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.

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

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

                  Equations
                    Instances For