Documentation

Std.Time.Date.Unit.Weekday

source
inductive Std.Time.Weekday :
Type

Defines the enumeration for days of the week. Each variant corresponds to a day of the week.

Instances For
    source
    @[implicit_reducible]
    instance Std.Time.instReprWeekday :
    Repr Weekday
    source
    def Std.Time.instReprWeekday.repr :
    Weekday → Nat → Std.Format
    Instances For
      source
      @[implicit_reducible]
      instance Std.Time.instInhabitedWeekday :
      Inhabited Weekday
      source
      def Std.Time.instInhabitedWeekday.default :
      Weekday
      Instances For
        source
        @[implicit_reducible]
        instance Std.Time.instDecidableEqWeekday :
        DecidableEq Weekday
        source
        def Std.Time.Weekday.Ordinal :
        Type

        Ordinal represents a bounded value for weekdays, which ranges between 1 and 7.

        Instances For
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instReprOrdinal :
          Repr Ordinal
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instDecidableEqOrdinal :
          DecidableEq Ordinal
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instLTOrdinal :
          LT Ordinal
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instLEOrdinal :
          LE Ordinal
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instDecidableLeOrdinal {x y : Ordinal} :
          Decidable (x ≤ y)
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instDecidableLtOrdinal {x y : Ordinal} :
          Decidable (x < y)
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instOfNatOrdinal {n : Nat} :
          OfNat Ordinal n
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instInhabitedOrdinal :
          Inhabited Ordinal
          source
          @[implicit_reducible]
          instance Std.Time.Weekday.instOrdOrdinal :
          Ord Ordinal
          source
          instance Std.Time.Weekday.instTransOrdOrdinal :
          TransOrd Ordinal
          source
          instance Std.Time.Weekday.instLawfulEqOrdOrdinal :
          LawfulEqOrd Ordinal
          source
          def Std.Time.Weekday.ofOrdinal :
          Ordinal → Weekday

          Converts a Ordinal representing a day index into a corresponding Weekday. This function is useful for mapping numerical representations to days of the week.

          Instances For
            source
            def Std.Time.Weekday.toOrdinal :
            Weekday → Ordinal

            Converts a Weekday to a Ordinal.

            Instances For
              source
              @[implicit_reducible]
              instance Std.Time.Weekday.instOrd :
              Ord Weekday
              source
              instance Std.Time.Weekday.instTransOrd :
              TransOrd Weekday
              source
              theorem Std.Time.Weekday.toOrdinal.inj {a b : Weekday} (h : a.toOrdinal = b.toOrdinal) :
              a = b
              source
              instance Std.Time.Weekday.instLawfulEqOrd :
              LawfulEqOrd Weekday
              source
              def Std.Time.Weekday.toNat :
              Weekday → Nat

              Converts a Weekday to a Nat.

              Instances For
                source
                def Std.Time.Weekday.ofNat? :
                Nat → Option Weekday

                Converts a Nat to an Option Weekday.

                Instances For
                  source
                  @[inline]
                  def Std.Time.Weekday.ofNat! (n : Nat) :
                  Weekday

                  Converts a Nat to a Weekday. Panics if the value provided is invalid.

                  Instances For
                    source
                    def Std.Time.Weekday.next :
                    Weekday → Weekday

                    Gets the next Weekday.

                    Instances For
                      source
                      def Std.Time.Weekday.isWeekend :
                      Weekday → Bool

                      Check if it's a weekend.

                      Instances For