TypeDB values

Lean representations of TypeDB 3 value types that keep every value exact: Decimal (TypeDB's 19-digit fixed point), Duration (months, days and nanoseconds, which do not normalise into each other), DatetimeTZ (an instant plus the zone it was written in) and IID.

Value and Concept are the raw shapes the native layer produces. Their constructor order and field order are mirrored by ffi/typedb_lean.c; change both together.

structure TypeDB.Decimal : Type

An exact decimal integer + fractional · 10⁻¹⁹ with fractional < 10¹⁹, TypeDB's representation. Negative values have a negative integer and a non-negative fractional, so -1.5 is ⟨-2, 5 · 10¹⁸⟩.

• integer : Int64
• fractional : UInt64

@[instance_reducible]

instance TypeDB.instDecidableEqDecimal : DecidableEq Decimal

Equations

• TypeDB.instDecidableEqDecimal = TypeDB.instDecidableEqDecimal.decEq

def TypeDB.instDecidableEqDecimal.decEq (x✝ x✝¹ : Decimal) : Decidable (x✝ = x✝¹)

Equations

• TypeDB.instDecidableEqDecimal.decEq { integer := a, fractional := a_1 } { integer := b, fractional := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def TypeDB.instReprDecimal.repr : Decimal → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instReprDecimal : Repr Decimal

Equations

• TypeDB.instReprDecimal = { reprPrec := TypeDB.instReprDecimal.repr }

@[instance_reducible]

instance TypeDB.instInhabitedDecimal : Inhabited Decimal

Equations

• TypeDB.instInhabitedDecimal = { default := TypeDB.instInhabitedDecimal.default }

def TypeDB.instHashableDecimal.hash : Decimal → UInt64

Equations

• TypeDB.instHashableDecimal.hash { integer := a, fractional := a_1 } = mixHash (mixHash 0 (hash a)) (hash a_1)

@[instance_reducible]

instance TypeDB.instHashableDecimal : Hashable Decimal

Equations

• TypeDB.instHashableDecimal = { hash := TypeDB.instHashableDecimal.hash }

def TypeDB.Decimal.scale : Nat

10¹⁹, the number of fractional units in one.

Equations

• TypeDB.Decimal.scale = 10 ^ 19

def TypeDB.Decimal.toScaled (d : Decimal) : Int

The value multiplied by 10¹⁹, as an integer.

Equations

• d.toScaled = d.integer.toInt * ↑TypeDB.Decimal.scale + ↑d.fractional.toNat

def TypeDB.Decimal.ofScaled (n : Int) : Decimal

The decimal n · 10⁻¹⁹; the integer part wraps around if it does not fit in Int64.

Equations

• TypeDB.Decimal.ofScaled n = { integer := Int64.ofInt (n.fdiv ↑TypeDB.Decimal.scale), fractional := UInt64.ofNat (n.fmod ↑TypeDB.Decimal.scale).toNat }

def TypeDB.Decimal.ofInt (n : Int) : Decimal

Equations

• TypeDB.Decimal.ofInt n = TypeDB.Decimal.ofScaled (n * ↑TypeDB.Decimal.scale)

@[instance_reducible]

instance TypeDB.Decimal.instOfNat (n : Nat) : OfNat Decimal n

Equations

• TypeDB.Decimal.instOfNat n = { ofNat := TypeDB.Decimal.ofInt ↑n }

@[instance_reducible]

instance TypeDB.Decimal.instAdd : Add Decimal

Equations

• TypeDB.Decimal.instAdd = { add := fun (a b : TypeDB.Decimal) => TypeDB.Decimal.ofScaled (a.toScaled + b.toScaled) }

@[instance_reducible]

instance TypeDB.Decimal.instSub : Sub Decimal

Equations

• TypeDB.Decimal.instSub = { sub := fun (a b : TypeDB.Decimal) => TypeDB.Decimal.ofScaled (a.toScaled - b.toScaled) }

@[instance_reducible]

instance TypeDB.Decimal.instNeg : Neg Decimal

Equations

• TypeDB.Decimal.instNeg = { neg := fun (a : TypeDB.Decimal) => TypeDB.Decimal.ofScaled (-a.toScaled) }

@[instance_reducible]

instance TypeDB.Decimal.instMul : Mul Decimal

Equations

• TypeDB.Decimal.instMul = { mul := fun (a b : TypeDB.Decimal) => TypeDB.Decimal.ofScaled ((a.toScaled * b.toScaled).tdiv ↑TypeDB.Decimal.scale) }

@[instance_reducible]

instance TypeDB.Decimal.instOrd : Ord Decimal

Equations

• TypeDB.Decimal.instOrd = { compare := fun (a b : TypeDB.Decimal) => compare a.toScaled b.toScaled }

@[instance_reducible]

instance TypeDB.Decimal.instLT : LT Decimal

Equations

• TypeDB.Decimal.instLT = { lt := fun (a b : TypeDB.Decimal) => a.toScaled < b.toScaled }

@[instance_reducible]

instance TypeDB.Decimal.instLE : LE Decimal

Equations

• TypeDB.Decimal.instLE = { le := fun (a b : TypeDB.Decimal) => a.toScaled ≤ b.toScaled }

@[instance_reducible]

instance TypeDB.Decimal.instDecidableLt (a b : Decimal) : Decidable (a < b)

Equations

• a.instDecidableLt b = Std.instDecidableLT a.toScaled b.toScaled

@[instance_reducible]

instance TypeDB.Decimal.instDecidableLe (a b : Decimal) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = Std.instDecidableLE a.toScaled b.toScaled

def TypeDB.Decimal.toString (d : Decimal) : String

Plain decimal notation with no trailing zeros, e.g. -1.5, 3.0.

Equations

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

@[instance_reducible]

instance TypeDB.Decimal.instToString : ToString Decimal

Equations

• TypeDB.Decimal.instToString = { toString := TypeDB.Decimal.toString }

def TypeDB.Decimal.ofString? (s : String) : Option Decimal

Parses [-]digits[.digits][dec] with at most 19 fractional digits.

Equations

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

structure TypeDB.Duration : Type

A TypeDB duration. Months, days and nanoseconds are kept apart because their lengths vary: a month is not a fixed number of days and a day is not always 24 hours.

• months : UInt32
• days : UInt32
• nanos : UInt64

def TypeDB.instDecidableEqDuration.decEq (x✝ x✝¹ : Duration) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TypeDB.instDecidableEqDuration : DecidableEq Duration

Equations

• TypeDB.instDecidableEqDuration = TypeDB.instDecidableEqDuration.decEq

@[instance_reducible]

instance TypeDB.instReprDuration : Repr Duration

Equations

• TypeDB.instReprDuration = { reprPrec := TypeDB.instReprDuration.repr }

def TypeDB.instReprDuration.repr : Duration → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedDuration : Inhabited Duration

Equations

• TypeDB.instInhabitedDuration = { default := TypeDB.instInhabitedDuration.default }

def TypeDB.instHashableDuration.hash : Duration → UInt64

Equations

• TypeDB.instHashableDuration.hash { months := a, days := a_1, nanos := a_2 } = mixHash (mixHash (mixHash 0 (hash a)) (hash a_1)) (hash a_2)

@[instance_reducible]

instance TypeDB.instHashableDuration : Hashable Duration

Equations

• TypeDB.instHashableDuration = { hash := TypeDB.instHashableDuration.hash }

def TypeDB.Duration.nanosPerSecond : Nat

Equations

• TypeDB.Duration.nanosPerSecond = 1000000000

def TypeDB.Duration.toISO (d : Duration) : String

ISO 8601 notation, as TypeQL writes duration literals: P1Y2M3DT4H5M6.5S.

Equations

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

@[instance_reducible]

instance TypeDB.Duration.instToString : ToString Duration

Equations

• TypeDB.Duration.instToString = { toString := TypeDB.Duration.toISO }

def TypeDB.Duration.ofSeconds (s : Nat) : Duration

Equations

• TypeDB.Duration.ofSeconds s = { nanos := UInt64.ofNat (s * TypeDB.Duration.nanosPerSecond) }

inductive TypeDB.Zone : Type

How a datetime-tz names its zone.

• iana (name : String) : Zone

  An IANA zone such as Europe/London.

• fixed (offsetSeconds : Int32) : Zone

  A fixed offset from UTC, in seconds.

def TypeDB.instDecidableEqZone.decEq (x✝ x✝¹ : Zone) : Decidable (x✝ = x✝¹)

Equations

• TypeDB.instDecidableEqZone.decEq (TypeDB.Zone.iana a) (TypeDB.Zone.iana b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• TypeDB.instDecidableEqZone.decEq (TypeDB.Zone.iana name) (TypeDB.Zone.fixed offsetSeconds) = isFalse ⋯
• TypeDB.instDecidableEqZone.decEq (TypeDB.Zone.fixed offsetSeconds) (TypeDB.Zone.iana name) = isFalse ⋯
• TypeDB.instDecidableEqZone.decEq (TypeDB.Zone.fixed a) (TypeDB.Zone.fixed b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.instDecidableEqZone : DecidableEq Zone

Equations

• TypeDB.instDecidableEqZone = TypeDB.instDecidableEqZone.decEq

@[instance_reducible]

instance TypeDB.instReprZone : Repr Zone

Equations

• TypeDB.instReprZone = { reprPrec := TypeDB.instReprZone.repr }

def TypeDB.instReprZone.repr : Zone → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedZone : Inhabited Zone

Equations

• TypeDB.instInhabitedZone = { default := TypeDB.instInhabitedZone.default }

structure TypeDB.DatetimeTZ : Type

A TypeDB datetime-tz: the instant (UTC seconds and nanoseconds since the Unix epoch), the zone it is expressed in, and the zone's UTC offset at that instant. The offset is what lets the value be printed back as local time without loading zone rules.

• seconds : Int64
• nanos : UInt32
• zone : Zone
• offsetSeconds : Int32

def TypeDB.instDecidableEqDatetimeTZ.decEq (x✝ x✝¹ : DatetimeTZ) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance TypeDB.instDecidableEqDatetimeTZ : DecidableEq DatetimeTZ

Equations

• TypeDB.instDecidableEqDatetimeTZ = TypeDB.instDecidableEqDatetimeTZ.decEq

@[instance_reducible]

instance TypeDB.instReprDatetimeTZ : Repr DatetimeTZ

Equations

• TypeDB.instReprDatetimeTZ = { reprPrec := TypeDB.instReprDatetimeTZ.repr }

def TypeDB.instReprDatetimeTZ.repr : DatetimeTZ → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedDatetimeTZ : Inhabited DatetimeTZ

Equations

• TypeDB.instInhabitedDatetimeTZ = { default := TypeDB.instInhabitedDatetimeTZ.default }

structure TypeDB.IID : Type

An instance identifier, as TypeDB prints it (0x1e00…).

• hex : String

def TypeDB.instDecidableEqIID.decEq (x✝ x✝¹ : IID) : Decidable (x✝ = x✝¹)

Equations

• TypeDB.instDecidableEqIID.decEq { hex := a } { hex := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance TypeDB.instDecidableEqIID : DecidableEq IID

Equations

• TypeDB.instDecidableEqIID = TypeDB.instDecidableEqIID.decEq

def TypeDB.instHashableIID.hash : IID → UInt64

Equations

• TypeDB.instHashableIID.hash { hex := a } = mixHash 0 (hash a)

@[instance_reducible]

instance TypeDB.instHashableIID : Hashable IID

Equations

• TypeDB.instHashableIID = { hash := TypeDB.instHashableIID.hash }

@[instance_reducible]

instance TypeDB.instReprIID : Repr IID

Equations

• TypeDB.instReprIID = { reprPrec := TypeDB.instReprIID.repr }

def TypeDB.instReprIID.repr : IID → Nat → Std.Format

Equations

• TypeDB.instReprIID.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "hex" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.hex)).group) " }"

@[instance_reducible]

instance TypeDB.instInhabitedIID : Inhabited IID

Equations

• TypeDB.instInhabitedIID = { default := TypeDB.instInhabitedIID.default }

def TypeDB.instOrdIID.ord : IID → IID → Ordering

Equations

• TypeDB.instOrdIID.ord { hex := a } { hex := b } = (compare a b).then Ordering.eq

@[instance_reducible]

instance TypeDB.instOrdIID : Ord IID

Equations

• TypeDB.instOrdIID = { compare := TypeDB.instOrdIID.ord }

@[instance_reducible]

instance TypeDB.instToStringIID : ToString IID

Equations

• TypeDB.instToStringIID = { toString := TypeDB.IID.hex }

inductive TypeDB.Value : Type

A value as the native layer reports it. Constructor and field order are mirrored by ffi/typedb_lean.c.

• bool (b : Bool) : Value
• integer (i : Int64) : Value
• double (d : Float) : Value
• decimal (integer : Int64) (fractional : UInt64) : Value
• string (s : String) : Value
• date (seconds : Int64) : Value

  A date, as the seconds since the Unix epoch of its midnight.

• datetime (seconds : Int64) (nanos : UInt32) : Value

  A datetime without zone, as UTC seconds and nanoseconds since the Unix epoch.

• datetimeTz (seconds : Int64) (nanos : UInt32) (zone : String) (offset : Int32) (fixed : Bool) : Value

  offset is only meaningful when fixed; IANA zones report their name and offset 0.

• duration (months days : UInt32) (nanos : UInt64) : Value

@[instance_reducible]

instance TypeDB.instReprValue : Repr Value

Equations

• TypeDB.instReprValue = { reprPrec := TypeDB.instReprValue.repr }

def TypeDB.instReprValue.repr : Value → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedValue : Inhabited Value

Equations

• TypeDB.instInhabitedValue = { default := TypeDB.instInhabitedValue.default }

def TypeDB.instBEqValue.beq : Value → Value → Bool

Equations

• TypeDB.instBEqValue.beq (TypeDB.Value.bool a) (TypeDB.Value.bool b) = (a == b)
• TypeDB.instBEqValue.beq (TypeDB.Value.integer a) (TypeDB.Value.integer b) = (a == b)
• TypeDB.instBEqValue.beq (TypeDB.Value.double a) (TypeDB.Value.double b) = (a == b)
• TypeDB.instBEqValue.beq (TypeDB.Value.decimal a a_1) (TypeDB.Value.decimal b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqValue.beq (TypeDB.Value.string a) (TypeDB.Value.string b) = (a == b)
• TypeDB.instBEqValue.beq (TypeDB.Value.date a) (TypeDB.Value.date b) = (a == b)
• TypeDB.instBEqValue.beq (TypeDB.Value.datetime a a_1) (TypeDB.Value.datetime b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqValue.beq (TypeDB.Value.datetimeTz a a_1 a_2 a_3 a_4) (TypeDB.Value.datetimeTz b b_1 b_2 b_3 b_4) = (a == b && (a_1 == b_1 && (a_2 == b_2 && (a_3 == b_3 && a_4 == b_4))))
• TypeDB.instBEqValue.beq (TypeDB.Value.duration a a_1 a_2) (TypeDB.Value.duration b b_1 b_2) = (a == b && (a_1 == b_1 && a_2 == b_2))
• TypeDB.instBEqValue.beq x✝¹ x✝ = false

@[instance_reducible]

instance TypeDB.instBEqValue : BEq Value

Equations

• TypeDB.instBEqValue = { beq := TypeDB.instBEqValue.beq }

def TypeDB.Value.typeName : Value → String

The TypeDB name of the value's type, used in decode errors.

Equations

• (TypeDB.Value.bool a).typeName = "boolean"
• (TypeDB.Value.integer a).typeName = "integer"
• (TypeDB.Value.double a).typeName = "double"
• (TypeDB.Value.decimal a a_1).typeName = "decimal"
• (TypeDB.Value.string a).typeName = "string"
• (TypeDB.Value.date a).typeName = "date"
• (TypeDB.Value.datetime a a_1).typeName = "datetime"
• (TypeDB.Value.datetimeTz a a_1 a_2 a_3 a_4).typeName = "datetime-tz"
• (TypeDB.Value.duration a a_1 a_2).typeName = "duration"

inductive TypeDB.Concept : Type

A concept in an answer row. Constructor and field order are mirrored by ffi/typedb_lean.c. Fields the decoder did not ask for (see Plan) are left as empty strings.

• entity (iid label : String) : Concept
• relation (iid label : String) : Concept
• attribute (label : String) (value : Value) : Concept
• value (v : Value) : Concept
• entityType (label : String) : Concept
• relationType (label : String) : Concept
• attributeType (label : String) : Concept
• roleType (label : String) : Concept

@[instance_reducible]

instance TypeDB.instReprConcept : Repr Concept

Equations

• TypeDB.instReprConcept = { reprPrec := TypeDB.instReprConcept.repr }

def TypeDB.instReprConcept.repr : Concept → Nat → Std.Format

Equations

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

@[instance_reducible]

instance TypeDB.instInhabitedConcept : Inhabited Concept

Equations

• TypeDB.instInhabitedConcept = { default := TypeDB.instInhabitedConcept.default }

def TypeDB.instBEqConcept.beq : Concept → Concept → Bool

Equations

• TypeDB.instBEqConcept.beq (TypeDB.Concept.entity a a_1) (TypeDB.Concept.entity b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.relation a a_1) (TypeDB.Concept.relation b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.attribute a a_1) (TypeDB.Concept.attribute b b_1) = (a == b && a_1 == b_1)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.value a) (TypeDB.Concept.value b) = (a == b)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.entityType a) (TypeDB.Concept.entityType b) = (a == b)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.relationType a) (TypeDB.Concept.relationType b) = (a == b)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.attributeType a) (TypeDB.Concept.attributeType b) = (a == b)
• TypeDB.instBEqConcept.beq (TypeDB.Concept.roleType a) (TypeDB.Concept.roleType b) = (a == b)
• TypeDB.instBEqConcept.beq x✝¹ x✝ = false

@[instance_reducible]

instance TypeDB.instBEqConcept : BEq Concept

Equations

• TypeDB.instBEqConcept = { beq := TypeDB.instBEqConcept.beq }

def TypeDB.Concept.value? : Concept → Option Value

The value of an attribute or value concept.

Equations

• (TypeDB.Concept.attribute label v).value? = some v
• (TypeDB.Concept.value v).value? = some v
• x✝.value? = none

def TypeDB.Concept.iid? : Concept → Option IID

The IID of an entity or relation.

Equations

• (TypeDB.Concept.entity i label).iid? = some { hex := i }
• (TypeDB.Concept.relation i label).iid? = some { hex := i }
• x✝.iid? = none

def TypeDB.Concept.label? : Concept → Option String

The type label of an instance, or the label of a type.

Equations

• (TypeDB.Concept.entity iid l).label? = some l
• (TypeDB.Concept.relation iid l).label? = some l
• (TypeDB.Concept.attribute l value).label? = some l
• (TypeDB.Concept.entityType l).label? = some l
• (TypeDB.Concept.relationType l).label? = some l
• (TypeDB.Concept.attributeType l).label? = some l
• (TypeDB.Concept.roleType l).label? = some l
• (TypeDB.Concept.value v).label? = none

def TypeDB.Concept.describe : Concept → String

A short description used in decode errors.

Equations

• (TypeDB.Concept.entity a a_1).describe = "entity"
• (TypeDB.Concept.relation a a_1).describe = "relation"
• (TypeDB.Concept.attribute a a_1).describe = toString a_1.typeName ++ toString " attribute"
• (TypeDB.Concept.value a).describe = toString a.typeName ++ toString " value"
• (TypeDB.Concept.entityType a).describe = "entity type"
• (TypeDB.Concept.relationType a).describe = "relation type"
• (TypeDB.Concept.attributeType a).describe = "attribute type"
• (TypeDB.Concept.roleType a).describe = "role type"

Conversions to and from Std.Time

def TypeDB.Time.secondsPerDay : Int

Equations

• TypeDB.Time.secondsPerDay = 86400

def TypeDB.Time.timestampOf (seconds : Int64) (nanos : UInt32) : Std.Time.Timestamp

Equations

• TypeDB.Time.timestampOf seconds nanos = Std.Time.Timestamp.ofNanosecondsSinceUnixEpoch (Std.Time.Nanosecond.Offset.ofInt (seconds.toInt * 1000000000 + ↑nanos.toNat))

def TypeDB.Time.splitTimestamp (t : Std.Time.Timestamp) : Int64 × UInt32

UTC seconds and sub-second nanoseconds of a timestamp.

Equations

• TypeDB.Time.splitTimestamp t = (Int64.ofInt (t.toNanosecondsSinceUnixEpoch.val.fdiv 1000000000), UInt32.ofNat (t.toNanosecondsSinceUnixEpoch.val.fmod 1000000000).toNat)

def TypeDB.Time.plainDateOfSeconds (seconds : Int64) : Std.Time.PlainDate

Equations

• TypeDB.Time.plainDateOfSeconds seconds = Std.Time.PlainDate.ofEpochDay (Std.Time.Day.Offset.ofInt (seconds.toInt.fdiv TypeDB.Time.secondsPerDay))

def TypeDB.Time.secondsOfPlainDate (d : Std.Time.PlainDate) : Int64

Equations

• TypeDB.Time.secondsOfPlainDate d = Int64.ofInt (d.toEpochDay.val * TypeDB.Time.secondsPerDay)

def TypeDB.Time.plainDateTimeOf (seconds : Int64) (nanos : UInt32) : Std.Time.PlainDateTime

Equations

• TypeDB.Time.plainDateTimeOf seconds nanos = (Std.Time.DateTime.ofTimestamp (TypeDB.Time.timestampOf seconds nanos) Std.Time.TimeZone.ZoneRules.UTC).toPlainDateTime

def TypeDB.Time.splitPlainDateTime (pdt : Std.Time.PlainDateTime) : Int64 × UInt32

Equations

• TypeDB.Time.splitPlainDateTime pdt = TypeDB.Time.splitTimestamp (pdt.toTimestamp Std.Time.TimeZone.ZoneRules.UTC)

def TypeDB.DatetimeTZ.timestamp (d : DatetimeTZ) : Std.Time.Timestamp

Equations

• d.timestamp = TypeDB.Time.timestampOf d.seconds d.nanos

def TypeDB.DatetimeTZ.localTime (d : DatetimeTZ) : Std.Time.PlainDateTime

The local wall time in the value's zone.

Equations

• d.localTime = TypeDB.Time.plainDateTimeOf (d.seconds + Int64.ofInt d.offsetSeconds.toInt) d.nanos

def TypeDB.DatetimeTZ.toDateTime (d : DatetimeTZ) : Std.Time.DateTime

The value as a Std.Time.DateTime whose zone is fixed at the value's offset. The instant and local time are exact; date arithmetic across a DST change needs toDateTimeWithRules.

Equations

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

def TypeDB.DatetimeTZ.toDateTimeWithRules (d : DatetimeTZ) : IO Std.Time.DateTime

The value as a Std.Time.DateTime with the full rules of its IANA zone.

Equations

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

def TypeDB.DatetimeTZ.ofDateTime (dt : Std.Time.DateTime) (iana : Option String := none) : DatetimeTZ

The instant of a Std.Time.DateTime, at its current offset. Pass iana to keep the zone's name, e.g. Europe/London; otherwise the value carries a fixed offset.

Equations

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

def TypeDB.DatetimeTZ.ofLocal (pdt : Std.Time.PlainDateTime) (iana : String) : IO DatetimeTZ

A local time in an IANA zone, resolved with the zone's rules.

Equations

• TypeDB.DatetimeTZ.ofLocal pdt iana = do let rules ← Std.Time.Database.defaultGetZoneRules iana pure (TypeDB.DatetimeTZ.ofDateTime (Std.Time.DateTime.ofPlainDateTime pdt rules) (some iana))

def TypeDB.DatetimeTZ.ofLocalFixed (pdt : Std.Time.PlainDateTime) (offsetSeconds : Int32) : DatetimeTZ

A local time at a fixed UTC offset in seconds.

Equations

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