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).
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Toml.Time.zero = { hour := 0, minute := 0, second := 0 }
Instances For
Equations
- Lake.Toml.Time.instOfNat = { ofNat := Lake.Toml.Time.zero }
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Lake.Toml.Time.instToString = { toString := Lake.Toml.Time.toString }
Equations
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 ⋯
Instances For
Equations
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Instances For
Equations
- Lake.Toml.DateTime.instToString = { toString := Lake.Toml.DateTime.toString }