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

@[implicit_reducible]

instance Lake.Toml.instInhabitedTime : Inhabited Time

Equations

• Lake.Toml.instInhabitedTime = { default := Lake.Toml.instInhabitedTime.default }

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

Equations

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

@[implicit_reducible]

instance Lake.Toml.instDecidableEqTime : DecidableEq Time

Equations

• Lake.Toml.instDecidableEqTime = Lake.Toml.instDecidableEqTime.decEq

@[reducible, inline]

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

Equations

• Lake.Toml.Time.IsValidHour h = (h ≤ 23)

@[reducible, inline]

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

Equations

• Lake.Toml.Time.IsValidMinute m = (m ≤ 59)

@[reducible, inline]

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

Equations

• Lake.Toml.Time.IsValidSecond s = (s ≤ 60)

def Lake.Toml.Time.zero : Time

Equations

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

@[implicit_reducible]

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

Equations

• Lake.Toml.Time.instOfNat = { ofNat := Lake.Toml.Time.zero }

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

Equations

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

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

Equations

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

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

Equations

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

@[implicit_reducible]

instance Lake.Toml.Time.instToString : ToString Time

Equations

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

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

@[implicit_reducible]

instance Lake.Toml.instInhabitedDateTime : Inhabited DateTime

Equations

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

@[implicit_reducible]

instance Lake.Toml.instDecidableEqDateTime : DecidableEq DateTime

Equations

• Lake.Toml.instDecidableEqDateTime = Lake.Toml.instDecidableEqDateTime.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.offsetDateTime date time offset?) (Lake.Toml.DateTime.localDateTime date_1 time_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.offsetDateTime date time offset?) (Lake.Toml.DateTime.localDate date_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.offsetDateTime date time offset?) (Lake.Toml.DateTime.localTime time_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDateTime date time) (Lake.Toml.DateTime.offsetDateTime date_1 time_1 offset?) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDateTime date time) (Lake.Toml.DateTime.localDate date_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDateTime date time) (Lake.Toml.DateTime.localTime time_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDate date) (Lake.Toml.DateTime.offsetDateTime date_1 time offset?) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDate date) (Lake.Toml.DateTime.localDateTime date_1 time) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDate a) (Lake.Toml.DateTime.localDate b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localDate date) (Lake.Toml.DateTime.localTime time) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localTime time) (Lake.Toml.DateTime.offsetDateTime date time_1 offset?) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localTime time) (Lake.Toml.DateTime.localDateTime date time_1) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localTime time) (Lake.Toml.DateTime.localDate date) = isFalse ⋯
• Lake.Toml.instDecidableEqDateTime.decEq (Lake.Toml.DateTime.localTime a) (Lake.Toml.DateTime.localTime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Lake.Toml.instCoeDateDateTime : Coe Date DateTime

Equations

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

@[implicit_reducible]

instance Lake.Toml.instCoeTimeDateTime : Coe Time DateTime

Equations

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

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

Equations

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

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

Equations

• One or more equations did not get rendered due to their size.
• (Lake.Toml.DateTime.offsetDateTime d t o?).toString = toString d ++ toString "T" ++ toString t ++ toString "Z"
• (Lake.Toml.DateTime.localDateTime d t).toString = toString d ++ toString "T" ++ toString t
• (Lake.Toml.DateTime.localDate d).toString = d.toString
• (Lake.Toml.DateTime.localTime t).toString = t.toString

@[implicit_reducible]

instance Lake.Toml.DateTime.instToString : ToString DateTime

Equations

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