This file defines Cedar values and results.

inductive Cedar.Spec.Error : Type

• entityDoesNotExist : Error
• attrDoesNotExist : Error
• tagDoesNotExist : Error
• typeError : Error
• arithBoundsError : Error
• extensionError : Error

@[reducible, inline]

abbrev Cedar.Spec.Result (α : Type u_1) : Type u_1

Equations

• Cedar.Spec.Result α = Except Cedar.Spec.Error α

@[reducible, inline]

abbrev Cedar.Spec.Id : Type

Equations

• Cedar.Spec.Id = String

structure Cedar.Spec.Name : Type

• id : Id
• path : List Id

instance Cedar.Spec.instToStringName : ToString Name

Equations

• Cedar.Spec.instToStringName = { toString := fun (n : Cedar.Spec.Name) => String.join (List.map (fun (s : Cedar.Spec.Id) => toString s ++ toString "::") n.path) ++ n.id }

@[reducible, inline]

abbrev Cedar.Spec.EntityType : Type

Equations

• Cedar.Spec.EntityType = Cedar.Spec.Name

instance Cedar.Spec.instToStringEntityType : ToString EntityType

Equations

• Cedar.Spec.instToStringEntityType = { toString := fun (ety : Cedar.Spec.EntityType) => have n := ety; toString n }

structure Cedar.Spec.EntityUID : Type

• ty : EntityType
• eid : String

instance Cedar.Spec.instToStringEntityUID : ToString EntityUID

Equations

• Cedar.Spec.instToStringEntityUID = { toString := fun (euid : Cedar.Spec.EntityUID) => toString euid.ty ++ toString "::\"" ++ toString euid.eid ++ toString "\"" }

inductive Cedar.Spec.Prim : Type

• bool (b : Bool) : Prim
• int (i : Int64) : Prim
• string (s : String) : Prim
• entityUID (uid : EntityUID) : Prim

@[reducible, inline]

abbrev Cedar.Spec.Attr : Type

Equations

• Cedar.Spec.Attr = String

inductive Cedar.Spec.Value : Type

• prim (p : Prim) : Value
• set (s : Data.Set Value) : Value
• record (m : Data.Map Attr Value) : Value
• ext (x : Ext) : Value

theorem Cedar.Spec.Value.sizeOf_set' (s : Data.Set Value) : sizeOf (set s) = 1 + sizeOf s

theorem Cedar.Spec.Value.sizeOf_record' (m : Data.Map Attr Value) : sizeOf (record m) = 1 + sizeOf m

def Cedar.Spec.Value.asEntityUID : Value → Result EntityUID

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID uid)).asEntityUID = Except.ok uid
• x✝.asEntityUID = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.Value.asSet : Value → Result (Data.Set Value)

Equations

• (Cedar.Spec.Value.set s).asSet = Except.ok s
• x✝.asSet = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.Value.asBool : Value → Result Bool

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b)).asBool = Except.ok b
• x✝.asBool = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.Value.asString : Value → Result String

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s)).asString = Except.ok s
• x✝.asString = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.Value.asInt : Value → Result Int64

Equations

• (Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i)).asInt = Except.ok i
• x✝.asInt = Except.error Cedar.Spec.Error.typeError

def Cedar.Spec.Result.as {α : Type u_1} (β : Type u_2) [Coe α (Result β)] : Result α → Result β

Equations

• Cedar.Spec.Result.as β (Except.ok v) = Coe.coe v
• Cedar.Spec.Result.as β (Except.error e) = Except.error e

instance Cedar.Spec.instCoeBoolValue : Coe Bool Value

Equations

• Cedar.Spec.instCoeBoolValue = { coe := fun (b : Bool) => Cedar.Spec.Value.prim (Cedar.Spec.Prim.bool b) }

instance Cedar.Spec.instCoeInt64Value : Coe Int64 Value

Equations

• Cedar.Spec.instCoeInt64Value = { coe := fun (i : Int64) => Cedar.Spec.Value.prim (Cedar.Spec.Prim.int i) }

instance Cedar.Spec.instCoeStringValue : Coe String Value

Equations

• Cedar.Spec.instCoeStringValue = { coe := fun (s : String) => Cedar.Spec.Value.prim (Cedar.Spec.Prim.string s) }

instance Cedar.Spec.instCoeEntityUIDValue : Coe EntityUID Value

Equations

• Cedar.Spec.instCoeEntityUIDValue = { coe := fun (e : Cedar.Spec.EntityUID) => Cedar.Spec.Value.prim (Cedar.Spec.Prim.entityUID e) }

instance Cedar.Spec.instCoePrimValue : Coe Prim Value

Equations

• Cedar.Spec.instCoePrimValue = { coe := fun (p : Cedar.Spec.Prim) => Cedar.Spec.Value.prim p }

instance Cedar.Spec.instCoeExtValue : Coe Ext Value

Equations

• Cedar.Spec.instCoeExtValue = { coe := fun (x : Cedar.Spec.Ext) => Cedar.Spec.Value.ext x }

instance Cedar.Spec.instCoeSetValue : Coe (Data.Set Value) Value

Equations

• Cedar.Spec.instCoeSetValue = { coe := fun (s : Cedar.Data.Set Cedar.Spec.Value) => Cedar.Spec.Value.set s }

instance Cedar.Spec.instCoeMapAttrValue : Coe (Data.Map Attr Value) Value

Equations

• Cedar.Spec.instCoeMapAttrValue = { coe := fun (r : Cedar.Data.Map Cedar.Spec.Attr Cedar.Spec.Value) => Cedar.Spec.Value.record r }

instance Cedar.Spec.instCoeValueResultBool : Coe Value (Result Bool)

Equations

• Cedar.Spec.instCoeValueResultBool = { coe := fun (v : Cedar.Spec.Value) => v.asBool }

instance Cedar.Spec.instCoeValueResultInt64 : Coe Value (Result Int64)

Equations

• Cedar.Spec.instCoeValueResultInt64 = { coe := fun (v : Cedar.Spec.Value) => v.asInt }

instance Cedar.Spec.instCoeValueResultString : Coe Value (Result String)

Equations

• Cedar.Spec.instCoeValueResultString = { coe := fun (v : Cedar.Spec.Value) => v.asString }

instance Cedar.Spec.instCoeValueResultEntityUID : Coe Value (Result EntityUID)

Equations

• Cedar.Spec.instCoeValueResultEntityUID = { coe := fun (v : Cedar.Spec.Value) => v.asEntityUID }

instance Cedar.Spec.instCoeValueResultSet : Coe Value (Result (Data.Set Value))

Equations

• Cedar.Spec.instCoeValueResultSet = { coe := fun (v : Cedar.Spec.Value) => v.asSet }

instance Cedar.Spec.instReprExcept_cedar {ε✝ : Type u_1} {α✝ : Type u_2} [Repr ε✝] [Repr α✝] : Repr (Except ε✝ α✝)

Equations

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

def Cedar.Spec.instReprExcept_cedar.repr {ε✝ : Type u_1} {α✝ : Type u_2} [Repr ε✝] [Repr α✝] : Except ε✝ α✝ → Nat → Std.Format

Equations

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

def Cedar.Spec.instDecidableEqExcept_cedar.decEq {ε✝ : Type u_1} {α✝ : Type u_2} [DecidableEq ε✝] [DecidableEq α✝] (x✝ x✝¹ : Except ε✝ α✝) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqExcept_cedar.decEq (Except.error a) (Except.error b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqExcept_cedar.decEq (Except.error a) (Except.ok a_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqExcept_cedar.decEq (Except.ok a) (Except.error a_1) = isFalse ⋯
• Cedar.Spec.instDecidableEqExcept_cedar.decEq (Except.ok a) (Except.ok b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqExcept_cedar {ε✝ : Type u_1} {α✝ : Type u_2} [DecidableEq ε✝] [DecidableEq α✝] : DecidableEq (Except ε✝ α✝)

Equations

• Cedar.Spec.instDecidableEqExcept_cedar = Cedar.Spec.instDecidableEqExcept_cedar.decEq

def Cedar.Spec.instBEqExcept_cedar.beq {ε✝ : Type u_1} {α✝ : Type u_2} [BEq ε✝] [BEq α✝] : Except ε✝ α✝ → Except ε✝ α✝ → Bool

Equations

• Cedar.Spec.instBEqExcept_cedar.beq (Except.error a) (Except.error b) = (a == b)
• Cedar.Spec.instBEqExcept_cedar.beq (Except.ok a) (Except.ok b) = (a == b)
• Cedar.Spec.instBEqExcept_cedar.beq x✝¹ x✝ = false

instance Cedar.Spec.instBEqExcept_cedar {ε✝ : Type u_1} {α✝ : Type u_2} [BEq ε✝] [BEq α✝] : BEq (Except ε✝ α✝)

Equations

• Cedar.Spec.instBEqExcept_cedar = { beq := Cedar.Spec.instBEqExcept_cedar.beq }

instance Cedar.Spec.instReprError : Repr Error

Equations

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

def Cedar.Spec.instReprError.repr : Error → Nat → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Spec.instReprError.repr Cedar.Spec.Error.typeError prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Cedar.Spec.Error.typeError")).group prec✝

instance Cedar.Spec.instDecidableEqError : DecidableEq Error

Equations

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

instance Cedar.Spec.instReprName : Repr Name

Equations

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

def Cedar.Spec.instReprName.repr : Name → Nat → Std.Format

Equations

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

instance Cedar.Spec.instDecidableEqName : DecidableEq Name

Equations

• Cedar.Spec.instDecidableEqName = Cedar.Spec.instDecidableEqName.decEq

def Cedar.Spec.instDecidableEqName.decEq (x✝ x✝¹ : Name) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqName.decEq { id := a, path := a_1 } { id := b, path := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

instance Cedar.Spec.instInhabitedName : Inhabited Name

Equations

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

def Cedar.Spec.instInhabitedName.default : Name

Equations

• Cedar.Spec.instInhabitedName.default = { id := default, path := default }

instance Cedar.Spec.instToJsonName : Lean.ToJson Name

Equations

• Cedar.Spec.instToJsonName = { toJson := Cedar.Spec.instToJsonName.toJson }

def Cedar.Spec.instToJsonName.toJson : Name → Lean.Json

Equations

• Cedar.Spec.instToJsonName.toJson x✝ = Lean.Json.mkObj [[("id", Lean.toJson x✝.id)], [("path", Lean.toJson x✝.path)]].flatten

instance Cedar.Spec.instDecidableEqEntityType : DecidableEq EntityType

Equations

• Cedar.Spec.instDecidableEqEntityType = Cedar.Spec.instDecidableEqName

instance Cedar.Spec.instInhabitedEntityType : Inhabited EntityType

Equations

• Cedar.Spec.instInhabitedEntityType = Cedar.Spec.instInhabitedName

instance Cedar.Spec.instReprEntityType : Repr EntityType

Equations

• Cedar.Spec.instReprEntityType = Cedar.Spec.instReprName

instance Cedar.Spec.instReprEntityUID : Repr EntityUID

Equations

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

def Cedar.Spec.instReprEntityUID.repr : EntityUID → Nat → Std.Format

Equations

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

instance Cedar.Spec.instDecidableEqEntityUID : DecidableEq EntityUID

Equations

• Cedar.Spec.instDecidableEqEntityUID = Cedar.Spec.instDecidableEqEntityUID.decEq

def Cedar.Spec.instDecidableEqEntityUID.decEq (x✝ x✝¹ : EntityUID) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqEntityUID.decEq { ty := a, eid := a_1 } { ty := b, eid := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

def Cedar.Spec.instInhabitedEntityUID.default : EntityUID

Equations

• Cedar.Spec.instInhabitedEntityUID.default = { ty := default, eid := default }

instance Cedar.Spec.instInhabitedEntityUID : Inhabited EntityUID

Equations

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

def Cedar.Spec.instToJsonEntityUID.toJson : EntityUID → Lean.Json

Equations

• Cedar.Spec.instToJsonEntityUID.toJson x✝ = Lean.Json.mkObj [[("ty", Lean.toJson x✝.ty)], [("eid", Lean.toJson x✝.eid)]].flatten

instance Cedar.Spec.instToJsonEntityUID : Lean.ToJson EntityUID

Equations

• Cedar.Spec.instToJsonEntityUID = { toJson := Cedar.Spec.instToJsonEntityUID.toJson }

def Cedar.Spec.instReprPrim.repr : Prim → Nat → Std.Format

Equations

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

instance Cedar.Spec.instReprPrim : Repr Prim

Equations

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

def Cedar.Spec.instDecidableEqPrim.decEq (x✝ x✝¹ : Prim) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.bool a) (Cedar.Spec.Prim.bool b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.bool b) (Cedar.Spec.Prim.int i) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.bool b) (Cedar.Spec.Prim.string s) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.bool b) (Cedar.Spec.Prim.entityUID uid) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.int i) (Cedar.Spec.Prim.bool b) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.int a) (Cedar.Spec.Prim.int b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.int i) (Cedar.Spec.Prim.string s) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.int i) (Cedar.Spec.Prim.entityUID uid) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.string s) (Cedar.Spec.Prim.bool b) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.string s) (Cedar.Spec.Prim.int i) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.string a) (Cedar.Spec.Prim.string b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.string s) (Cedar.Spec.Prim.entityUID uid) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.entityUID uid) (Cedar.Spec.Prim.bool b) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.entityUID uid) (Cedar.Spec.Prim.int i) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.entityUID uid) (Cedar.Spec.Prim.string s) = isFalse ⋯
• Cedar.Spec.instDecidableEqPrim.decEq (Cedar.Spec.Prim.entityUID a) (Cedar.Spec.Prim.entityUID b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Cedar.Spec.instDecidableEqPrim : DecidableEq Prim

Equations

• Cedar.Spec.instDecidableEqPrim = Cedar.Spec.instDecidableEqPrim.decEq

def Cedar.Spec.instInhabitedPrim.default : Prim

Equations

• Cedar.Spec.instInhabitedPrim.default = Cedar.Spec.Prim.bool default

instance Cedar.Spec.instInhabitedPrim : Inhabited Prim

Equations

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

partial def Cedar.Spec.instReprValue.repr : Value → Nat → Std.Format

instance Cedar.Spec.instReprValue : Repr Value

Equations

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

def Cedar.Spec.instInhabitedValue.default : Value

Equations

• Cedar.Spec.instInhabitedValue.default = Cedar.Spec.Value.prim default

instance Cedar.Spec.instInhabitedValue : Inhabited Value

Equations

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

instance Cedar.Spec.instLawfulBEqExcept_cedar {α : Type u_1} {ε : Type u_2} [BEq α] [BEq ε] [LawfulBEq α] [LawfulBEq ε] : LawfulBEq (Except ε α)

def Cedar.Spec.decValue (v₁ v₂ : Value) : Decidable (v₁ = v₂)

Equations

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

instance Cedar.Spec.instDecidableEqValue : DecidableEq Value

Equations

• Cedar.Spec.instDecidableEqValue = Cedar.Spec.decValue

def Cedar.Spec.Name.lt (a b : Name) : Bool

Equations

• a.lt b = decide (a.id :: a.path < b.id :: b.path)

instance Cedar.Spec.instLTName : LT Name

Equations

• Cedar.Spec.instLTName = { lt := fun (a b : Cedar.Spec.Name) => a.lt b = true }

instance Cedar.Spec.Name.decLt (a b : Name) : Decidable (a < b)

Equations

• a.decLt b = if h : a.lt b = true then isTrue h else isFalse h

def Cedar.Spec.EntityUID.lt (a b : EntityUID) : Bool

Equations

• a.lt b = decide (a.ty < b.ty ∨ a.ty = b.ty ∧ a.eid < b.eid)

instance Cedar.Spec.instLTEntityUID : LT EntityUID

Equations

• Cedar.Spec.instLTEntityUID = { lt := fun (a b : Cedar.Spec.EntityUID) => a.lt b = true }

instance Cedar.Spec.EntityUID.decLt (a b : EntityUID) : Decidable (a < b)

Equations

• a.decLt b = if h : a.lt b = true then isTrue h else isFalse h

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

Equations

• (Cedar.Spec.Prim.bool b₁).lt (Cedar.Spec.Prim.bool b₂) = decide (b₁ < b₂)
• (Cedar.Spec.Prim.int i₁).lt (Cedar.Spec.Prim.int i₂) = decide (i₁ < i₂)
• (Cedar.Spec.Prim.string s₁).lt (Cedar.Spec.Prim.string s₂) = decide (s₁ < s₂)
• (Cedar.Spec.Prim.entityUID uid₁).lt (Cedar.Spec.Prim.entityUID uid₂) = decide (uid₁ < uid₂)
• (Cedar.Spec.Prim.bool b).lt (Cedar.Spec.Prim.int i) = true
• (Cedar.Spec.Prim.bool b).lt (Cedar.Spec.Prim.string s) = true
• (Cedar.Spec.Prim.bool b).lt (Cedar.Spec.Prim.entityUID uid) = true
• (Cedar.Spec.Prim.int i).lt (Cedar.Spec.Prim.string s) = true
• (Cedar.Spec.Prim.int i).lt (Cedar.Spec.Prim.entityUID uid) = true
• (Cedar.Spec.Prim.string s).lt (Cedar.Spec.Prim.entityUID uid) = true
• x✝¹.lt x✝ = false

instance Cedar.Spec.instLTPrim : LT Prim

Equations

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

instance Cedar.Spec.Prim.decLt (a b : Prim) : Decidable (a < b)

Equations

• a.decLt b = if h : a.lt b = true then isTrue h else isFalse h

@[irreducible]

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

Equations

• (Cedar.Spec.Value.prim p₁).lt (Cedar.Spec.Value.prim p₂) = decide (p₁ < p₂)
• (Cedar.Spec.Value.set (Cedar.Data.Set.mk vs₁)).lt (Cedar.Spec.Value.set (Cedar.Data.Set.mk vs₂)) = Cedar.Spec.Values.lt vs₁ vs₂
• (Cedar.Spec.Value.record (Cedar.Data.Map.mk avs₁)).lt (Cedar.Spec.Value.record (Cedar.Data.Map.mk avs₂)) = Cedar.Spec.ValueAttrs.lt avs₁ avs₂
• (Cedar.Spec.Value.ext x_2).lt (Cedar.Spec.Value.ext y) = decide (x_2 < y)
• (Cedar.Spec.Value.prim p).lt (Cedar.Spec.Value.set s) = true
• (Cedar.Spec.Value.prim p).lt (Cedar.Spec.Value.record m) = true
• (Cedar.Spec.Value.prim p).lt (Cedar.Spec.Value.ext x_2) = true
• (Cedar.Spec.Value.set s).lt (Cedar.Spec.Value.record m) = true
• (Cedar.Spec.Value.set s).lt (Cedar.Spec.Value.ext x_2) = true
• (Cedar.Spec.Value.set s).lt (Cedar.Spec.Value.prim p) = false
• (Cedar.Spec.Value.record m).lt (Cedar.Spec.Value.ext x_2) = true
• (Cedar.Spec.Value.record m).lt (Cedar.Spec.Value.prim p) = false
• (Cedar.Spec.Value.record m).lt (Cedar.Spec.Value.set s) = false
• (Cedar.Spec.Value.ext x_2).lt (Cedar.Spec.Value.prim p) = false
• (Cedar.Spec.Value.ext x_2).lt (Cedar.Spec.Value.set s) = false
• (Cedar.Spec.Value.ext x_2).lt (Cedar.Spec.Value.record m) = false

@[irreducible]

def Cedar.Spec.Values.lt : List Value → List Value → Bool

Equations

• Cedar.Spec.Values.lt [] [] = false
• Cedar.Spec.Values.lt [] x✝ = true
• Cedar.Spec.Values.lt x✝ [] = false
• Cedar.Spec.Values.lt (v₁ :: vs₁) (v₂ :: vs₂) = (v₁.lt v₂ || decide (v₁ = v₂) && Cedar.Spec.Values.lt vs₁ vs₂)

@[irreducible]

def Cedar.Spec.ValueAttrs.lt : List (Attr × Value) → List (Attr × Value) → Bool

Equations

• Cedar.Spec.ValueAttrs.lt [] [] = false
• Cedar.Spec.ValueAttrs.lt [] x✝ = true
• Cedar.Spec.ValueAttrs.lt x✝ [] = false
• Cedar.Spec.ValueAttrs.lt ((a₁, v₁) :: avs₁) ((a₂, v₂) :: avs₂) = (decide (a₁ < a₂) || decide (a₁ = a₂) && v₁.lt v₂ || decide (a₁ = a₂) && decide (v₁ = v₂) && Cedar.Spec.ValueAttrs.lt avs₁ avs₂)

instance Cedar.Spec.instLTValue : LT Value

Equations

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

instance Cedar.Spec.Value.decLt (a b : Value) : Decidable (a < b)

Equations

• a.decLt b = if h : a.lt b = true then isTrue h else isFalse h