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

instance Lake.Toml.instInhabitedTime : Inhabited Lake.Toml.Time

Equations

• Lake.Toml.instInhabitedTime = { default := { hour := default, minute := default, second := default, fracExponent := default, fracMantissa := default } }

instance Lake.Toml.instDecidableEqTime : DecidableEq Lake.Toml.Time

Equations

• Lake.Toml.instDecidableEqTime = Lake.Toml.decEqTime✝

@[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 : Lake.Toml.Time

Equations

• Lake.Toml.Time.zero = { hour := 0, minute := 0, second := 0, fracExponent := 0, fracMantissa := 0 }

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

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

Equations

• One or more equations did not get rendered due to their size.

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

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

instance Lake.Toml.Time.instToString : ToString Lake.Toml.Time

Equations

• Lake.Toml.Time.instToString = { toString := Lake.Toml.Time.toString }

inductive Lake.Toml.DateTime : Type

A TOML date-time.

• offsetDateTime: Lake.Date → Lake.Toml.Time → optParam (Option (Bool × Lake.Toml.Time)) none → Lake.Toml.DateTime
• localDateTime: Lake.Date → Lake.Toml.Time → Lake.Toml.DateTime
• localDate: Lake.Date → Lake.Toml.DateTime
• localTime: Lake.Toml.Time → Lake.Toml.DateTime

instance Lake.Toml.instInhabitedDateTime : Inhabited Lake.Toml.DateTime

Equations

• Lake.Toml.instInhabitedDateTime = { default := Lake.Toml.DateTime.offsetDateTime default default default }

instance Lake.Toml.instDecidableEqDateTime : DecidableEq Lake.Toml.DateTime

Equations

• Lake.Toml.instDecidableEqDateTime = Lake.Toml.decEqDateTime✝

instance Lake.Toml.instCoeDateDateTime : Coe Lake.Date Lake.Toml.DateTime

Equations

• Lake.Toml.instCoeDateDateTime = { coe := Lake.Toml.DateTime.localDate }

instance Lake.Toml.instCoeTimeDateTime : Coe Lake.Toml.Time Lake.Toml.DateTime

Equations

• Lake.Toml.instCoeTimeDateTime = { coe := Lake.Toml.DateTime.localTime }

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

Equations

• One or more equations did not get rendered due to their size.

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

instance Lake.Toml.DateTime.instToString : ToString Lake.Toml.DateTime