This file defines Cedar extension functions.

inductive Cedar.Spec.ExtFun : Type

• decimal : ExtFun
• lessThan : ExtFun
• lessThanOrEqual : ExtFun
• greaterThan : ExtFun
• greaterThanOrEqual : ExtFun
• ip : ExtFun
• isIpv4 : ExtFun
• isIpv6 : ExtFun
• isLoopback : ExtFun
• isMulticast : ExtFun
• isInRange : ExtFun
• datetime : ExtFun
• duration : ExtFun
• offset : ExtFun
• durationSince : ExtFun
• toDate : ExtFun
• toTime : ExtFun
• toMilliseconds : ExtFun
• toSeconds : ExtFun
• toMinutes : ExtFun
• toHours : ExtFun
• toDays : ExtFun

def Cedar.Spec.res {α : Type u_1} [Coe α Ext] : Option α → Result Value

Equations

• Cedar.Spec.res (some v) = Except.ok (Cedar.Spec.Value.ext (Coe.coe v))
• Cedar.Spec.res none = Except.error Cedar.Spec.Error.extensionError

def Cedar.Spec.call : ExtFun → List Value → Result Value

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.call Cedar.Spec.ExtFun.decimal [Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)] = Cedar.Spec.res (Cedar.Spec.Ext.Decimal.decimal s)
• Cedar.Spec.call Cedar.Spec.ExtFun.ip [Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)] = Cedar.Spec.res (Cedar.Spec.Ext.IPAddr.ip s)
• Cedar.Spec.call Cedar.Spec.ExtFun.isIpv4 [Cedar.Spec.Value.ext (Cedar.Spec.Ext.ipaddr a)] = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (Cedar.Spec.Ext.IPAddr.IPNet.isV4 a)))
• Cedar.Spec.call Cedar.Spec.ExtFun.isIpv6 [Cedar.Spec.Value.ext (Cedar.Spec.Ext.ipaddr a)] = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (Cedar.Spec.Ext.IPAddr.IPNet.isV6 a)))
• Cedar.Spec.call Cedar.Spec.ExtFun.isLoopback [Cedar.Spec.Value.ext (Cedar.Spec.Ext.ipaddr a)] = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (Cedar.Spec.Ext.IPAddr.IPNet.isLoopback a)))
• Cedar.Spec.call Cedar.Spec.ExtFun.isMulticast [Cedar.Spec.Value.ext (Cedar.Spec.Ext.ipaddr a)] = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool (Cedar.Spec.Ext.IPAddr.IPNet.isMulticast a)))
• Cedar.Spec.call Cedar.Spec.ExtFun.datetime [Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)] = Cedar.Spec.res (Cedar.Spec.Ext.Datetime.parse s)
• Cedar.Spec.call Cedar.Spec.ExtFun.duration [Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)] = Cedar.Spec.res (Cedar.Spec.Ext.Datetime.Duration.parse s)
• Cedar.Spec.call Cedar.Spec.ExtFun.offset [Cedar.Spec.Value.ext (Cedar.Spec.Ext.datetime dt), Cedar.Spec.Value.ext (Cedar.Spec.Ext.duration dur)] = Cedar.Spec.res (dt.offset dur)
• Cedar.Spec.call Cedar.Spec.ExtFun.durationSince [Cedar.Spec.Value.ext (Cedar.Spec.Ext.datetime d₁), Cedar.Spec.Value.ext (Cedar.Spec.Ext.datetime d₂)] = Cedar.Spec.res (d₁.durationSince d₂)
• Cedar.Spec.call Cedar.Spec.ExtFun.toDate [Cedar.Spec.Value.ext (Cedar.Spec.Ext.datetime dt)] = Cedar.Spec.res dt.toDate
• Cedar.Spec.call Cedar.Spec.ExtFun.toTime [Cedar.Spec.Value.ext (Cedar.Spec.Ext.datetime dt)] = Except.ok (Cedar.Spec.Value.ext (Cedar.Spec.Ext.duration dt.toTime))
• Cedar.Spec.call Cedar.Spec.ExtFun.toDays [Cedar.Spec.Value.ext (Cedar.Spec.Ext.duration dur)] = Except.ok (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int (Cedar.Spec.Ext.Datetime.Duration.toDays dur)))
• Cedar.Spec.call x✝¹ x✝ = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.instReprExtFun.repr : ExtFun → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.decimal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.decimal")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.lessThan prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.lessThan")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.ip prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.ip")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.isIpv4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.isIpv4")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.isIpv6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.isIpv6")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.isInRange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.isInRange")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.datetime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.datetime")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.duration prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.duration")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.offset prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.offset")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toDate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toDate")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toTime prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toTime")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toSeconds prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toSeconds")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toMinutes prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toMinutes")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toHours prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toHours")).group prec✝
• Cedar.Spec.instReprExtFun.repr Cedar.Spec.ExtFun.toDays prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.ExtFun.toDays")).group prec✝

instance Cedar.Spec.instReprExtFun : Repr ExtFun

Equations

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

instance Cedar.Spec.instDecidableEqExtFun : DecidableEq ExtFun

Equations

• Cedar.Spec.instDecidableEqExtFun x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cedar.Spec.instInhabitedExtFun.default : ExtFun

Equations

• Cedar.Spec.instInhabitedExtFun.default = Cedar.Spec.ExtFun.decimal

instance Cedar.Spec.instInhabitedExtFun : Inhabited ExtFun

Equations

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