This file defines Cedar datetime values and functions.

structure Cedar.Spec.Ext.Datetime : Type

A datetime value is measured in milliseconds and constructed from a datetime string. A datetime string must be of one of the forms:

• YYYY-MM-DD (date only)
• YYYY-MM-DDThh:mm:ssZ (UTC)
• YYYY-MM-DDThh:mm:ss.SSSZ (UTC with millisecond precision)
• YYYY-MM-DDThh:mm:ss(+|-)hhmm (With timezone offset in hours and minutes)
• YYYY-MM-DDThh:mm:ss.SSS(+|-)hhmm (With timezone offset in hours and minutes and millisecond precision)

Regardless of the timezone, offset is always normalized to UTC.

The datetime type does not provide a way to create a datetime from a Unix timestamp. One of the readable formats listed above must be used instead.

• val : Int64

def Cedar.Spec.Ext.Datetime.lt (d₁ d₂ : Datetime) : Bool

Equations

• d₁.lt d₂ = decide (d₁.val < d₂.val)

def Cedar.Spec.Ext.Datetime.le (d₁ d₂ : Datetime) : Bool

Equations

• d₁.le d₂ = decide (d₁.val ≤ d₂.val)

instance Cedar.Spec.Ext.instLTDatetime : LT Datetime

Equations

• Cedar.Spec.Ext.instLTDatetime = { lt := fun (d₁ d₂ : Cedar.Spec.Ext.Datetime) => d₁.lt d₂ = true }

instance Cedar.Spec.Ext.instLEDatetime : LE Datetime

Equations

• Cedar.Spec.Ext.instLEDatetime = { le := fun (d₁ d₂ : Cedar.Spec.Ext.Datetime) => d₁.le d₂ = true }

instance Cedar.Spec.Ext.Datetime.decLt (d₁ d₂ : Datetime) : Decidable (d₁ < d₂)

Equations

• d₁.decLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h

instance Cedar.Spec.Ext.Datetime.decLe (d₁ d₂ : Datetime) : Decidable (d₁ ≤ d₂)

Equations

• d₁.decLe d₂ = if h : d₁.le d₂ = true then isTrue h else isFalse h

instance Cedar.Spec.Ext.instCoeInt64Datetime : Coe Int64 Datetime

Equations

• Cedar.Spec.Ext.instCoeInt64Datetime = { coe := fun (i : Int64) => { val := i } }

def Cedar.Spec.Ext.instReprDatetime.repr : Datetime → Nat → Std.Format

Equations

• Cedar.Spec.Ext.instReprDatetime.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "val" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.val)).group) " }"

instance Cedar.Spec.Ext.instReprDatetime : Repr Datetime

Equations

• Cedar.Spec.Ext.instReprDatetime = { reprPrec := Cedar.Spec.Ext.instReprDatetime.repr }

def Cedar.Spec.Ext.instInhabitedDatetime.default : Datetime

Equations

• Cedar.Spec.Ext.instInhabitedDatetime.default = { val := default }

instance Cedar.Spec.Ext.instInhabitedDatetime : Inhabited Datetime

Equations

• Cedar.Spec.Ext.instInhabitedDatetime = { default := Cedar.Spec.Ext.instInhabitedDatetime.default }

instance Cedar.Spec.Ext.instDecidableEqDatetime : DecidableEq Datetime

Equations

• Cedar.Spec.Ext.instDecidableEqDatetime = Cedar.Spec.Ext.instDecidableEqDatetime.decEq

def Cedar.Spec.Ext.instDecidableEqDatetime.decEq (x✝ x✝¹ : Datetime) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.Ext.instDecidableEqDatetime.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Cedar.Spec.Ext.Datetime.datetime? (i : Int) : Option Datetime

Equations

• Cedar.Spec.Ext.Datetime.datetime? i = do let a ← Int64.ofInt? i pure { val := a }

def Cedar.Spec.Ext.Datetime.parse (str : String) : Option Datetime

Equations

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

@[reducible, inline]

abbrev Cedar.Spec.Ext.Datetime.datetime (str : String) : Option Datetime

Equations

• Cedar.Spec.Ext.Datetime.datetime = Cedar.Spec.Ext.Datetime.parse

structure Cedar.Spec.Ext.Datetime.Duration : Type

A duration value is measured in milliseconds and constructed from a duration string. A duration string is a concatenated sequence of quantity-unit pairs where the quantity is a natural number and unit is one of the following:

• d (for days)
• h (for hours)
• m (for minutes)
• s (for seconds)
• ms (for milliseconds)

Duration strings are required to be ordered from largest unit to smallest unit, and contain one quantity per unit. Units with zero quantity may be omitted.

A duration may be negative. Negative duration strings must begin with -.

• val : Int64

def Cedar.Spec.Ext.Datetime.instReprDuration.repr : Duration → Nat → Std.Format

Equations

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

instance Cedar.Spec.Ext.Datetime.instReprDuration : Repr Duration

Equations

• Cedar.Spec.Ext.Datetime.instReprDuration = { reprPrec := Cedar.Spec.Ext.Datetime.instReprDuration.repr }

instance Cedar.Spec.Ext.Datetime.instInhabitedDuration : Inhabited Duration

Equations

• Cedar.Spec.Ext.Datetime.instInhabitedDuration = { default := Cedar.Spec.Ext.Datetime.instInhabitedDuration.default }

def Cedar.Spec.Ext.Datetime.instInhabitedDuration.default : Duration

Equations

• Cedar.Spec.Ext.Datetime.instInhabitedDuration.default = { val := default }

def Cedar.Spec.Ext.Datetime.instDecidableEqDuration.decEq (x✝ x✝¹ : Duration) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.Ext.Datetime.instDecidableEqDuration.decEq { val := a } { val := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.Ext.Datetime.instDecidableEqDuration : DecidableEq Duration

Equations

• Cedar.Spec.Ext.Datetime.instDecidableEqDuration = Cedar.Spec.Ext.Datetime.instDecidableEqDuration.decEq

def Cedar.Spec.Ext.Datetime.Duration.lt (d₁ d₂ : Duration) : Bool

Equations

• d₁.lt d₂ = decide (d₁.val < d₂.val)

def Cedar.Spec.Ext.Datetime.Duration.le (d₁ d₂ : Duration) : Bool

Equations

• d₁.le d₂ = decide (d₁.val ≤ d₂.val)

instance Cedar.Spec.Ext.Datetime.instLTDuration : LT Duration

Equations

• Cedar.Spec.Ext.Datetime.instLTDuration = { lt := fun (d₁ d₂ : Cedar.Spec.Ext.Datetime.Duration) => d₁.lt d₂ = true }

instance Cedar.Spec.Ext.Datetime.instLEDuration : LE Duration

Equations

• Cedar.Spec.Ext.Datetime.instLEDuration = { le := fun (d₁ d₂ : Cedar.Spec.Ext.Datetime.Duration) => d₁.le d₂ = true }

instance Cedar.Spec.Ext.Datetime.Duration.decLt (d₁ d₂ : Duration) : Decidable (d₁ < d₂)

Equations

• d₁.decLt d₂ = if h : d₁.lt d₂ = true then isTrue h else isFalse h

instance Cedar.Spec.Ext.Datetime.Duration.decLe (d₁ d₂ : Duration) : Decidable (d₁ ≤ d₂)

Equations

• d₁.decLe d₂ = if h : d₁.le d₂ = true then isTrue h else isFalse h

instance Cedar.Spec.Ext.Datetime.instCoeInt64Duration : Coe Int64 Duration

Equations

• Cedar.Spec.Ext.Datetime.instCoeInt64Duration = { coe := fun (i : Int64) => { val := i } }

def Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_SECOND : Int

Equations

• Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_SECOND = 1000

def Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_MINUTE : Int

Equations

• Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_MINUTE = 60000

def Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_HOUR : Int

Equations

• Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_HOUR = 3600000

def Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_DAY : Int

Equations

• Cedar.Spec.Ext.Datetime.MILLISECONDS_PER_DAY = 86400000

def Cedar.Spec.Ext.Datetime.duration? (i : Int) : Option Duration

Create a Duration from an Int representing its internal encoding. Most callers should use higher-level constructors, e.g., Duration.parse

Equations

• Cedar.Spec.Ext.Datetime.duration? i = do let a ← Int64.ofInt? i pure { val := a }

def Cedar.Spec.Ext.Datetime.Duration.parse (str : String) : Option Duration

Equations

• Cedar.Spec.Ext.Datetime.Duration.parse str = match Cedar.Spec.Ext.Datetime.isNegativeDuration✝ str with | (isNegative, restStr) => Cedar.Spec.Ext.Datetime.parseDuration?✝ isNegative restStr

def Cedar.Spec.Ext.Datetime.instReprDuration_1.repr : Duration → Nat → Std.Format

Equations

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

instance Cedar.Spec.Ext.Datetime.instReprDuration_1 : Repr Duration

Equations

• Cedar.Spec.Ext.Datetime.instReprDuration_1 = { reprPrec := Cedar.Spec.Ext.Datetime.instReprDuration_1.repr }

@[reducible, inline]

abbrev Cedar.Spec.Ext.Datetime.duration (str : String) : Option Duration

Equations

• Cedar.Spec.Ext.Datetime.duration = Cedar.Spec.Ext.Datetime.Duration.parse

def Cedar.Spec.Ext.Datetime.offset (datetime : Datetime) (duration : Duration) : Option Datetime

Equations

• datetime.offset duration = do let a ← datetime.val.add? duration.val pure { val := a }

def Cedar.Spec.Ext.Datetime.durationSince (datetime other : Datetime) : Option Duration

Equations

• datetime.durationSince other = do let a ← datetime.val.sub? other.val pure { val := a }

def Cedar.Spec.Ext.Datetime.toDate (datetime : Datetime) : Option Datetime

Equations

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

def Cedar.Spec.Ext.Datetime.toTime (datetime : Datetime) : Duration

Equations

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

def Cedar.Spec.Ext.Datetime.Duration.toMilliseconds (duration : Duration) : Int64

Equations

• duration.toMilliseconds = duration.val

def Cedar.Spec.Ext.Datetime.Duration.toSeconds (duration : Duration) : Int64

Equations

• duration.toSeconds = duration.toMilliseconds / 1000

def Cedar.Spec.Ext.Datetime.Duration.toMinutes (duration : Duration) : Int64

Equations

• duration.toMinutes = duration.toSeconds / 60

def Cedar.Spec.Ext.Datetime.Duration.toHours (duration : Duration) : Int64

Equations

• duration.toHours = duration.toMinutes / 60

def Cedar.Spec.Ext.Datetime.Duration.toDays (duration : Duration) : Int64

Equations

• duration.toDays = duration.toHours / 24