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