Documentation

Std.Time.Date.ValidDate

source
def Std.Time.ValidDate (leap : Bool) :
Type

Represents a valid date for a given year, considering whether it is a leap year. Example: (2, 29) is valid only if leap is true.

Equations
    Instances For
      source
      instance Std.Time.instInhabitedValidDate {l : Bool} :
      Inhabited (ValidDate l)
      Equations
        source
        instance Std.Time.instDecidableEqValidDate {leap : Bool} :
        DecidableEq (ValidDate leap)
        Equations
          source
          instance Std.Time.instOrdValidDate {leap : Bool} :
          Ord (ValidDate leap)
          Equations
            source
            instance Std.Time.instOrientedOrdValidDate {leap : Bool} :
            OrientedOrd (ValidDate leap)
            source
            instance Std.Time.instTransOrdValidDate {leap : Bool} :
            TransOrd (ValidDate leap)
            source
            instance Std.Time.instLawfulEqOrdValidDate {leap : Bool} :
            LawfulEqOrd (ValidDate leap)
            source
            def Std.Time.ValidDate.dayOfYear {leap : Bool} (ordinal : ValidDate leap) :
            Day.Ordinal.OfYear leap

            Transforms a tuple of a Month and a Day into a Day.Ordinal.OfYear.

            Equations
              Instances For
                source
                def Std.Time.ValidDate.ofOrdinal {leap : Bool} (ordinal : Day.Ordinal.OfYear leap) :
                ValidDate leap

                Transforms a Day.Ordinal.OfYear into a tuple of a Month and a Day.

                Equations
                  Instances For