This file contains the executable version of TypeEnv.WellFormed and related definitions.

inductive Cedar.Validation.EnvironmentValidationError : Type

• typeError (msg : String) : EnvironmentValidationError

instance Cedar.Validation.instToStringEnvironmentValidationError : ToString EnvironmentValidationError

Equations

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

@[reducible, inline]

abbrev Cedar.Validation.EnvironmentValidationResult : Type

Equations

• Cedar.Validation.EnvironmentValidationResult = Except Cedar.Validation.EnvironmentValidationError Unit

def Cedar.Validation.EntityType.validateWellFormed (env : TypeEnv) (ety : Spec.EntityType) : EnvironmentValidationResult

Equations

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

@[irreducible]

def Cedar.Validation.QualifiedType.validateWellFormed (env : TypeEnv) (qty : QualifiedType) : EnvironmentValidationResult

Equations

• Cedar.Validation.QualifiedType.validateWellFormed env (Cedar.Validation.Qualified.optional ty) = Cedar.Validation.CedarType.validateWellFormed env ty
• Cedar.Validation.QualifiedType.validateWellFormed env (Cedar.Validation.Qualified.required ty) = Cedar.Validation.CedarType.validateWellFormed env ty

@[irreducible]

def Cedar.Validation.validateAttrsWellFormed (env : TypeEnv) (rty : List (Spec.Attr × QualifiedType)) : EnvironmentValidationResult

Equations

• Cedar.Validation.validateAttrsWellFormed env [] = Except.ok ()
• Cedar.Validation.validateAttrsWellFormed env ((fst, qty) :: rest) = do Cedar.Validation.QualifiedType.validateWellFormed env qty Cedar.Validation.validateAttrsWellFormed env rest

@[irreducible]

def Cedar.Validation.CedarType.validateWellFormed (env : TypeEnv) (ty : CedarType) : EnvironmentValidationResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.CedarType.validateWellFormed env (Cedar.Validation.CedarType.bool bty) = Except.ok ()
• Cedar.Validation.CedarType.validateWellFormed env Cedar.Validation.CedarType.int = Except.ok ()
• Cedar.Validation.CedarType.validateWellFormed env Cedar.Validation.CedarType.string = Except.ok ()
• Cedar.Validation.CedarType.validateWellFormed env (Cedar.Validation.CedarType.entity ety) = Cedar.Validation.EntityType.validateWellFormed env ety
• Cedar.Validation.CedarType.validateWellFormed env ty_2.set = Cedar.Validation.CedarType.validateWellFormed env ty_2
• Cedar.Validation.CedarType.validateWellFormed env (Cedar.Validation.CedarType.ext xty) = Except.ok ()

@[irreducible]

def Cedar.Validation.CedarType.validateLifted (ty : CedarType) : EnvironmentValidationResult

Equations

• One or more equations did not get rendered due to their size.
• (Cedar.Validation.CedarType.bool Cedar.Validation.BoolType.anyBool).validateLifted = Except.ok ()
• (Cedar.Validation.CedarType.bool bty).validateLifted = Except.error (Cedar.Validation.EnvironmentValidationError.typeError (toString "bool type is not lifted"))
• Cedar.Validation.CedarType.int.validateLifted = Except.ok ()
• Cedar.Validation.CedarType.string.validateLifted = Except.ok ()
• (Cedar.Validation.CedarType.entity ety).validateLifted = Except.ok ()
• ty_2.set.validateLifted = ty_2.validateLifted
• (Cedar.Validation.CedarType.ext xty).validateLifted = Except.ok ()

def Cedar.Validation.StandardSchemaEntry.validateWellFormed (env : TypeEnv) (entry : StandardSchemaEntry) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.EntitySchemaEntry.validateWellFormed (env : TypeEnv) (entry : EntitySchemaEntry) : EnvironmentValidationResult

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.EntitySchemaEntry.validateWellFormed env (Cedar.Validation.EntitySchemaEntry.standard entry_2) = Cedar.Validation.StandardSchemaEntry.validateWellFormed env entry_2

def Cedar.Validation.EntitySchema.validateWellFormed (env : TypeEnv) (ets : EntitySchema) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.ActionSchemaEntry.validateWellFormed (env : TypeEnv) (entry : ActionSchemaEntry) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.ActionSchema.validateAcyclicActionHierarchy (acts : ActionSchema) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.ActionSchema.validateTransitiveActionHierarchy (acts : ActionSchema) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.ActionSchema.validateWellFormed (env : TypeEnv) (acts : ActionSchema) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.RequestType.validateWellFormed (env : TypeEnv) (reqty : RequestType) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.TypeEnv.validateWellFormed (env : TypeEnv) : EnvironmentValidationResult

Equations

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

def Cedar.Validation.Schema.validateWellFormed (schema : Schema) : EnvironmentValidationResult

Equations

• schema.validateWellFormed = schema.environments.forM Cedar.Validation.TypeEnv.validateWellFormed