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
    @[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
                      Instances For
                        Equations
                          Instances For
                            Equations
                              Instances For

                                A TOML date-time.

                                Instances For
                                  Equations
                                    Instances For
                                      Equations
                                        Instances For