inductive Cedar.Validation.PartialEntitySchemaEntry : Type

• defined (entry : EntitySchemaEntry) : PartialEntitySchemaEntry
• external (parents : Data.Set Spec.EntityType) : PartialEntitySchemaEntry

@[instance_reducible]

instance Cedar.Validation.instReprPartialEntitySchemaEntry : Repr PartialEntitySchemaEntry

Equations

• Cedar.Validation.instReprPartialEntitySchemaEntry = { reprPrec := Cedar.Validation.instReprPartialEntitySchemaEntry.repr }

def Cedar.Validation.instReprPartialEntitySchemaEntry.repr : PartialEntitySchemaEntry → Nat → Std.Format

Equations

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

def Cedar.Validation.PartialEntitySchemaEntry.isValidEntityEID (entry : PartialEntitySchemaEntry) (eid : String) : Bool

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).isValidEntityEID eid = a.isValidEntityEID eid
• (Cedar.Validation.PartialEntitySchemaEntry.external a).isValidEntityEID eid = true

def Cedar.Validation.PartialEntitySchemaEntry.tags? : PartialEntitySchemaEntry → Option (Option CedarType)

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).tags? = some a.tags?
• (Cedar.Validation.PartialEntitySchemaEntry.external a).tags? = none

def Cedar.Validation.PartialEntitySchemaEntry.attrs? : PartialEntitySchemaEntry → Option RecordType

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).attrs? = some a.attrs
• (Cedar.Validation.PartialEntitySchemaEntry.external a).attrs? = none

def Cedar.Validation.PartialEntitySchemaEntry.ancestors : PartialEntitySchemaEntry → Data.Set Spec.EntityType

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).ancestors = a.ancestors
• (Cedar.Validation.PartialEntitySchemaEntry.external a).ancestors = a

def Cedar.Validation.PartialEntitySchemaEntry.isStandard : PartialEntitySchemaEntry → Bool

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).isStandard = a.isStandard
• (Cedar.Validation.PartialEntitySchemaEntry.external a).isStandard = true

def Cedar.Validation.PartialEntitySchemaEntry.isExternal : PartialEntitySchemaEntry → Bool

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).isExternal = false
• (Cedar.Validation.PartialEntitySchemaEntry.external a).isExternal = true

def Cedar.Validation.PartialEntitySchemaEntry.toEntitySchemaEntry? : PartialEntitySchemaEntry → Option EntitySchemaEntry

Equations

• (Cedar.Validation.PartialEntitySchemaEntry.defined a).toEntitySchemaEntry? = some a
• (Cedar.Validation.PartialEntitySchemaEntry.external a).toEntitySchemaEntry? = none

def Cedar.Validation.PartialEntitySchemaEntry.withAncestors (ancestors : Data.Set Spec.EntityType) : PartialEntitySchemaEntry → PartialEntitySchemaEntry

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.PartialEntitySchemaEntry.withAncestors ancestors (Cedar.Validation.PartialEntitySchemaEntry.external a) = Cedar.Validation.PartialEntitySchemaEntry.external ancestors

@[instance_reducible]

instance Cedar.Validation.instCoeEntitySchemaEntryPartialEntitySchemaEntry : Coe EntitySchemaEntry PartialEntitySchemaEntry

Equations

• Cedar.Validation.instCoeEntitySchemaEntryPartialEntitySchemaEntry = { coe := Cedar.Validation.PartialEntitySchemaEntry.defined }

inductive Cedar.Validation.PartialActionSchemaEntry : Type

• defined (entry : ActionSchemaEntry) : PartialActionSchemaEntry
• external (parents : Data.Set Spec.EntityUID) : PartialActionSchemaEntry

def Cedar.Validation.instReprPartialActionSchemaEntry.repr : PartialActionSchemaEntry → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cedar.Validation.instReprPartialActionSchemaEntry : Repr PartialActionSchemaEntry

Equations

• Cedar.Validation.instReprPartialActionSchemaEntry = { reprPrec := Cedar.Validation.instReprPartialActionSchemaEntry.repr }

def Cedar.Validation.PartialActionSchemaEntry.ancestors : PartialActionSchemaEntry → Data.Set Spec.EntityUID

Equations

• (Cedar.Validation.PartialActionSchemaEntry.defined a).ancestors = a.ancestors
• (Cedar.Validation.PartialActionSchemaEntry.external a).ancestors = a

def Cedar.Validation.PartialActionSchemaEntry.isExternal : PartialActionSchemaEntry → Bool

Equations

• (Cedar.Validation.PartialActionSchemaEntry.defined a).isExternal = false
• (Cedar.Validation.PartialActionSchemaEntry.external a).isExternal = true

def Cedar.Validation.PartialActionSchemaEntry.toActionSchemaEntry? : PartialActionSchemaEntry → Option ActionSchemaEntry

Equations

• (Cedar.Validation.PartialActionSchemaEntry.defined a).toActionSchemaEntry? = some a
• (Cedar.Validation.PartialActionSchemaEntry.external a).toActionSchemaEntry? = none

def Cedar.Validation.PartialActionSchemaEntry.withAncestors (ancestors : Data.Set Spec.EntityUID) : PartialActionSchemaEntry → PartialActionSchemaEntry

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.PartialActionSchemaEntry.withAncestors ancestors (Cedar.Validation.PartialActionSchemaEntry.external a) = Cedar.Validation.PartialActionSchemaEntry.external ancestors

@[instance_reducible]

instance Cedar.Validation.instCoeActionSchemaEntryPartialActionSchemaEntry : Coe ActionSchemaEntry PartialActionSchemaEntry

Equations

• Cedar.Validation.instCoeActionSchemaEntryPartialActionSchemaEntry = { coe := Cedar.Validation.PartialActionSchemaEntry.defined }

@[reducible, inline]

abbrev Cedar.Validation.PartialEntitySchema : Type

Equations

• Cedar.Validation.PartialEntitySchema = Cedar.Data.Map Cedar.Spec.EntityType Cedar.Validation.PartialEntitySchemaEntry

@[reducible, inline]

abbrev Cedar.Validation.PartialActionSchema : Type

Equations

• Cedar.Validation.PartialActionSchema = Cedar.Data.Map Cedar.Spec.EntityUID Cedar.Validation.PartialActionSchemaEntry

structure Cedar.Validation.PartialSchema : Type

• ets : PartialEntitySchema
• acts : PartialActionSchema

def Cedar.Validation.instReprPartialSchema.repr : PartialSchema → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Cedar.Validation.instReprPartialSchema : Repr PartialSchema

Equations

• Cedar.Validation.instReprPartialSchema = { reprPrec := Cedar.Validation.instReprPartialSchema.repr }

def Cedar.Validation.Schema.toPartialSchema (s : Schema) : PartialSchema

Equations

• ↑s = { ets := Cedar.Data.Map.mapOnValues Cedar.Validation.PartialEntitySchemaEntry.defined s.ets, acts := Cedar.Data.Map.mapOnValues Cedar.Validation.PartialActionSchemaEntry.defined s.acts }

@[instance_reducible]

instance Cedar.Validation.instCoeSchemaPartialSchema : Coe Schema PartialSchema

Equations

• Cedar.Validation.instCoeSchemaPartialSchema = { coe := Cedar.Validation.Schema.toPartialSchema }

def Cedar.Validation.PartialSchema.isComplete (ps : PartialSchema) : Bool

Equations

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

def Cedar.Validation.PartialSchema.asSchema? (ps : PartialSchema) : Option Schema

Equations

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