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.

• Offset Date-Time: A full RFC 3339 date-time.
• Local Date-Time: An RFC 3339 date-time without the time zone.
• Local Date: The date portion of an RFC 3339 date-time (year-month-day).
• Local Time: The time portion of an RFC 3339 date-time (without time zone).

structure Lake.Toml.Time : Type

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.

• hour : Nat
• minute : Nat
• second : Nat
• fracExponent : Nat
• fracMantissa : Nat

def Lake.Toml.instInhabitedTime.default : Time

@[implicit_reducible]

instance Lake.Toml.instInhabitedTime : Inhabited Time

def Lake.Toml.instDecidableEqTime.decEq (x✝ x✝¹ : Time) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Lake.Toml.instDecidableEqTime : DecidableEq Time

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidHour (h : Nat) : Prop

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidMinute (m : Nat) : Prop

@[reducible, inline]

abbrev Lake.Toml.Time.IsValidSecond (s : Nat) : Prop

def Lake.Toml.Time.zero : Time

@[implicit_reducible]

instance Lake.Toml.Time.instOfNat : OfNat Time 0

def Lake.Toml.Time.ofValid? (hour minute second : Nat) : Option Time

def Lake.Toml.Time.ofString? (t : String) : Option Time

def Lake.Toml.Time.toString (t : Time) : String

@[implicit_reducible]

instance Lake.Toml.Time.instToString : ToString Time

inductive Lake.Toml.DateTime : Type

A TOML date-time.

• offsetDateTime (date : Date) (time : Time) (offset? : Option (Bool × Time) := none) : DateTime
• localDateTime (date : Date) (time : Time) : DateTime
• localDate (date : Date) : DateTime
• localTime (time : Time) : DateTime

def Lake.Toml.instInhabitedDateTime.default : DateTime

@[implicit_reducible]

instance Lake.Toml.instInhabitedDateTime : Inhabited DateTime

@[implicit_reducible]

instance Lake.Toml.instDecidableEqDateTime : DecidableEq DateTime

def Lake.Toml.instDecidableEqDateTime.decEq (x✝ x✝¹ : DateTime) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Lake.Toml.instCoeDateDateTime : Coe Date DateTime

@[implicit_reducible]

instance Lake.Toml.instCoeTimeDateTime : Coe Time DateTime

def Lake.Toml.DateTime.ofString? (dt : String) : Option DateTime

def Lake.Toml.DateTime.toString (dt : DateTime) : String

@[implicit_reducible]

instance Lake.Toml.DateTime.instToString : ToString DateTime