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.

structure Lake.Toml.Time :

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

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

Instances For
    Equations
    Instances For
      def Lake.Toml.instDecidableEqTime.decEq (x✝ x✝¹ : Time) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[reducible, inline]
        Equations
        Instances For
          @[reducible, inline]
          Equations
          Instances For
            @[reducible, inline]
            Equations
            Instances For
              Equations
              Instances For
                def Lake.Toml.Time.ofValid? (hour minute 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

                      A TOML date-time.

                      Instances For
                        def Lake.Toml.instDecidableEqDateTime.decEq (x✝ x✝¹ : DateTime) :
                        Decidable (x✝ = x✝¹)
                        Equations
                        Instances For
                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For