Documentation

Lake.Toml.Data.DateTime

TOML Date-Time #

Defines data types for representing a TOML date-time. TOML date-times are based on IETF RFC 3339 with some components optionally left out, creating four distinct variants.

def Lake.Toml.lpad (s : String) (c : Char) (len : Nat) :
Equations
Instances For
    def Lake.Toml.rpad (s : String) (c : Char) (len : Nat) :
    Equations
    Instances For
      def Lake.Toml.zpad (n : Nat) (len : Nat) :
      Equations
      Instances For
        structure Lake.Toml.Date :

        A TOML date (year-month-day).

        Instances For
          Equations
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              def Lake.Toml.Date.maxDay (y : Nat) (m : Nat) :
              Equations
              Instances For
                @[reducible, inline]
                abbrev Lake.Toml.Date.IsValidDay (y : Nat) (m : Nat) (d : Nat) :
                Equations
                Instances For
                  def Lake.Toml.Date.ofValid? (year : Nat) (month : Nat) (day : Nat) :
                  Equations
                  Instances For
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        structure Lake.Toml.Time :

                        A TOML time (hour:minute:second.fraction).

                        We do not represent whole time as seconds to due to the possibility of leap seconds in RFC 3339 times.

                        Instances For
                          Equations
                          • Lake.Toml.instInhabitedTime = { default := { hour := default, minute := default, second := default, fracExponent := default, fracMantissa := default } }
                          @[reducible, inline]
                          Equations
                          Instances For
                            @[reducible, inline]
                            Equations
                            Instances For
                              @[reducible, inline]
                              Equations
                              Instances For
                                Equations
                                Instances For
                                  def Lake.Toml.Time.ofValid? (hour : Nat) (minute : Nat) (second : Nat) :
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          Equations
                                          Instances For