This file defines Cedar entities.

@[reducible, inline]

abbrev Cedar.Spec.Tag : Type

Equations

• Cedar.Spec.Tag = String

structure Cedar.Spec.EntityData : Type

• attrs : Data.Map Attr Value
• ancestors : Data.Set EntityUID
• tags : Data.Map Tag Value

@[reducible, inline]

abbrev Cedar.Spec.Entities : Type

Equations

• Cedar.Spec.Entities = Cedar.Data.Map Cedar.Spec.EntityUID Cedar.Spec.EntityData

def Cedar.Spec.Entities.ancestors (es : Entities) (uid : EntityUID) : Result (Data.Set EntityUID)

Equations

• es.ancestors uid = do let d ← Cedar.Data.Map.findOrErr es uid Cedar.Spec.Error.entityDoesNotExist Except.ok d.ancestors

def Cedar.Spec.Entities.ancestorsOrEmpty (es : Entities) (uid : EntityUID) : Data.Set EntityUID

Equations

• es.ancestorsOrEmpty uid = match Cedar.Data.Map.find? es uid with | some d => d.ancestors | none => Cedar.Data.Set.empty

def Cedar.Spec.Entities.attrs (es : Entities) (uid : EntityUID) : Result (Data.Map Attr Value)

Equations

• es.attrs uid = do let d ← Cedar.Data.Map.findOrErr es uid Cedar.Spec.Error.entityDoesNotExist Except.ok d.attrs

def Cedar.Spec.Entities.attrsOrEmpty (es : Entities) (uid : EntityUID) : Data.Map Attr Value

Equations

• es.attrsOrEmpty uid = match Cedar.Data.Map.find? es uid with | some d => d.attrs | none => Cedar.Data.Map.empty

def Cedar.Spec.Entities.tags (es : Entities) (uid : EntityUID) : Result (Data.Map Tag Value)

Equations

• es.tags uid = do let d ← Cedar.Data.Map.findOrErr es uid Cedar.Spec.Error.entityDoesNotExist Except.ok d.tags

def Cedar.Spec.Entities.tagsOrEmpty (es : Entities) (uid : EntityUID) : Data.Map Tag Value

Equations

• es.tagsOrEmpty uid = match Cedar.Data.Map.find? es uid with | some d => d.tags | none => Cedar.Data.Map.empty

instance Cedar.Spec.instReprEntityData : Repr EntityData

Equations

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

def Cedar.Spec.instReprEntityData.repr : EntityData → Nat → Std.Format

Equations

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

def Cedar.Spec.instDecidableEqEntityData.decEq (x✝ x✝¹ : EntityData) : Decidable (x✝ = x✝¹)

Equations

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

instance Cedar.Spec.instDecidableEqEntityData : DecidableEq EntityData

Equations

• Cedar.Spec.instDecidableEqEntityData = Cedar.Spec.instDecidableEqEntityData.decEq

instance Cedar.Spec.instInhabitedEntityData : Inhabited EntityData

Equations

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

def Cedar.Spec.instInhabitedEntityData.default : EntityData

Equations

• Cedar.Spec.instInhabitedEntityData.default = { attrs := default, ancestors := default, tags := default }