This file defines Cedar extension values.

@[reducible, inline]

abbrev Cedar.Spec.IPAddr : Type

Equations

• Cedar.Spec.IPAddr = Cedar.Spec.Ext.IPAddr.IPNet

@[reducible, inline]

abbrev Cedar.Spec.Duration : Type

Equations

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

inductive Cedar.Spec.Ext : Type

• decimal (d : Decimal) : Ext
• ipaddr (ip : IPAddr) : Ext
• datetime (dt : Datetime) : Ext
• duration (dur : Duration) : Ext

def Cedar.Spec.Ext.lt : Ext → Ext → Bool

Ordering on extension types: .decimal < .ipaddr < .datetime < .duration

Equations

• (Cedar.Spec.Ext.decimal d₁).lt (Cedar.Spec.Ext.decimal d₂) = decide (d₁ < d₂)
• (Cedar.Spec.Ext.ipaddr ip₁).lt (Cedar.Spec.Ext.ipaddr ip₂) = decide (ip₁ < ip₂)
• (Cedar.Spec.Ext.datetime d₁).lt (Cedar.Spec.Ext.datetime d₂) = decide (d₁ < d₂)
• (Cedar.Spec.Ext.duration d₁).lt (Cedar.Spec.Ext.duration d₂) = decide (d₁ < d₂)
• (Cedar.Spec.Ext.decimal d).lt x✝ = true
• (Cedar.Spec.Ext.ipaddr ip).lt (Cedar.Spec.Ext.datetime dt) = true
• (Cedar.Spec.Ext.ipaddr ip).lt (Cedar.Spec.Ext.duration dur) = true
• (Cedar.Spec.Ext.datetime dt).lt (Cedar.Spec.Ext.duration dur) = true
• x✝¹.lt x✝ = false

def Cedar.Spec.instReprExt.repr : Ext → Nat → Std.Format

Equations

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

instance Cedar.Spec.instReprExt : Repr Ext

Equations

• Cedar.Spec.instReprExt = { reprPrec := Cedar.Spec.instReprExt.repr }

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

Equations

• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.decimal a) (Cedar.Spec.Ext.decimal b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.decimal d) (Cedar.Spec.Ext.ipaddr ip) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.decimal d) (Cedar.Spec.Ext.datetime dt) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.decimal d) (Cedar.Spec.Ext.duration dur) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.ipaddr ip) (Cedar.Spec.Ext.decimal d) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.ipaddr a) (Cedar.Spec.Ext.ipaddr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.ipaddr ip) (Cedar.Spec.Ext.datetime dt) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.ipaddr ip) (Cedar.Spec.Ext.duration dur) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.datetime dt) (Cedar.Spec.Ext.decimal d) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.datetime dt) (Cedar.Spec.Ext.ipaddr ip) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.datetime a) (Cedar.Spec.Ext.datetime b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.datetime dt) (Cedar.Spec.Ext.duration dur) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.duration dur) (Cedar.Spec.Ext.decimal d) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.duration dur) (Cedar.Spec.Ext.ipaddr ip) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.duration dur) (Cedar.Spec.Ext.datetime dt) = isFalse ⋯
• Cedar.Spec.instDecidableEqExt.decEq (Cedar.Spec.Ext.duration a) (Cedar.Spec.Ext.duration b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqExt : DecidableEq Ext

Equations

• Cedar.Spec.instDecidableEqExt = Cedar.Spec.instDecidableEqExt.decEq

def Cedar.Spec.instInhabitedExt.default : Ext

Equations

• Cedar.Spec.instInhabitedExt.default = Cedar.Spec.Ext.decimal default

instance Cedar.Spec.instInhabitedExt : Inhabited Ext

Equations

• Cedar.Spec.instInhabitedExt = { default := Cedar.Spec.instInhabitedExt.default }

instance Cedar.Spec.instLTExt : LT Ext

Equations

• Cedar.Spec.instLTExt = { lt := fun (x y : Cedar.Spec.Ext) => x.lt y = true }

instance Cedar.Spec.Ext.decLt (x y : Ext) : Decidable (x < y)

Equations

• x.decLt y = if h : x.lt y = true then isTrue h else isFalse h

instance Cedar.Spec.instCoeDecimalExt : Coe Ext.Decimal Ext

Equations

• Cedar.Spec.instCoeDecimalExt = { coe := fun (d : Cedar.Spec.Ext.Decimal) => Cedar.Spec.Ext.decimal d }

instance Cedar.Spec.instCoeIPAddrExt : Coe IPAddr Ext

Equations

• Cedar.Spec.instCoeIPAddrExt = { coe := fun (a : Cedar.Spec.IPAddr) => Cedar.Spec.Ext.ipaddr a }

instance Cedar.Spec.instCoeDatetimeExt : Coe Ext.Datetime Ext

Equations

• Cedar.Spec.instCoeDatetimeExt = { coe := fun (dt : Cedar.Spec.Ext.Datetime) => Cedar.Spec.Ext.datetime dt }

instance Cedar.Spec.instCoeDurationExt : Coe Duration Ext

Equations

• Cedar.Spec.instCoeDurationExt = { coe := fun (dur : Cedar.Spec.Duration) => Cedar.Spec.Ext.duration dur }