This file contains well-typedness definitions of TypedExpr

inductive Cedar.Spec.Prim.WellTyped (env : Validation.TypeEnv) : Prim → Validation.CedarType → Prop

• bool {env : Validation.TypeEnv} (b : Bool) : WellTyped env (Prim.bool b) (Validation.CedarType.bool Validation.BoolType.anyBool)
• int {env : Validation.TypeEnv} (i : Int64) : WellTyped env (Prim.int i) Validation.CedarType.int
• string {env : Validation.TypeEnv} (s : String) : WellTyped env (Prim.string s) Validation.CedarType.string
• entityUID {env : Validation.TypeEnv} (uid : EntityUID) (h₁ : env.ets.isValidEntityUID uid = true ∨ env.acts.contains uid = true) : WellTyped env (Prim.entityUID uid) (Validation.CedarType.entity uid.ty)

inductive Cedar.Spec.Var.WellTyped (env : Validation.TypeEnv) : Var → Validation.CedarType → Prop

• principal {env : Validation.TypeEnv} : WellTyped env Var.principal (Validation.CedarType.entity env.reqty.principal)
• resource {env : Validation.TypeEnv} : WellTyped env Var.resource (Validation.CedarType.entity env.reqty.resource)
• action {env : Validation.TypeEnv} : WellTyped env Var.action (Validation.CedarType.entity env.reqty.action.ty)
• context {env : Validation.TypeEnv} : WellTyped env Var.context (Validation.CedarType.record env.reqty.context).liftBoolTypes

inductive Cedar.Spec.UnaryOp.WellTyped : UnaryOp → Validation.TypedExpr → Validation.CedarType → Prop

• not {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : UnaryOp.not.WellTyped x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• neg {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) : UnaryOp.neg.WellTyped x₁ Validation.CedarType.int
• isEmpty {x₁ : Validation.TypedExpr} {eltTy : Validation.CedarType} (h₁ : x₁.typeOf = eltTy.set) : UnaryOp.isEmpty.WellTyped x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• like {x₁ : Validation.TypedExpr} {p : Pattern} (h₁ : x₁.typeOf = Validation.CedarType.string) : (UnaryOp.like p).WellTyped x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)
• is {x₁ : Validation.TypedExpr} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₂) : (UnaryOp.is ety₁).WellTyped x₁ (Validation.CedarType.bool Validation.BoolType.anyBool)

inductive Cedar.Spec.BinaryOp.WellTyped (env : Validation.TypeEnv) : BinaryOp → Validation.TypedExpr → Validation.TypedExpr → Validation.CedarType → Prop

• eq_lit {env : Validation.TypeEnv} {p₁ p₂ : Prim} {ty₁ ty₂ : Validation.CedarType} : WellTyped env BinaryOp.eq (Validation.TypedExpr.lit p₁ ty₁) (Validation.TypedExpr.lit p₂ ty₂) (Validation.CedarType.bool Validation.BoolType.anyBool)
• eq_entity {env : Validation.TypeEnv} {ety₁ ety₂ : EntityType} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : WellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• eq {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = x₂.typeOf) : WellTyped env BinaryOp.eq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• memₑ {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = Validation.CedarType.entity ety₂) : WellTyped env mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• memₛ {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ety₁ ety₂ : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety₁) (h₂ : x₂.typeOf = (Validation.CedarType.entity ety₂).set) : WellTyped env mem x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_int {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : WellTyped env less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_datetime {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : WellTyped env less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• less_duration {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : WellTyped env less x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_int {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : WellTyped env lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_datetime {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : WellTyped env lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessEq_duration {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : WellTyped env lessEq x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• add {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : WellTyped env BinaryOp.add x₁ x₂ Validation.CedarType.int
• sub {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : WellTyped env BinaryOp.sub x₁ x₂ Validation.CedarType.int
• mul {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.int) (h₂ : x₂.typeOf = Validation.CedarType.int) : WellTyped env BinaryOp.mul x₁ x₂ Validation.CedarType.int
• contains {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = x₂.typeOf.set) : WellTyped env BinaryOp.contains x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• containsAll {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : WellTyped env BinaryOp.containsAll x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• containsAny {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : x₁.typeOf = ty.set) (h₂ : x₂.typeOf = ty.set) : WellTyped env BinaryOp.containsAny x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• hasTag {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ety : EntityType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) : WellTyped env BinaryOp.hasTag x₁ x₂ (Validation.CedarType.bool Validation.BoolType.anyBool)
• getTag {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} {ety : EntityType} {ty : Validation.CedarType} (h₁ : x₁.typeOf = Validation.CedarType.entity ety) (h₂ : x₂.typeOf = Validation.CedarType.string) (h₃ : env.ets.tags? ety = some (some ty)) : WellTyped env BinaryOp.getTag x₁ x₂ ty.liftBoolTypes

inductive Cedar.Spec.ExtFun.WellTyped : ExtFun → List Validation.TypedExpr → Validation.CedarType → Prop

• decimal {s₁ : String} {d₁ : Ext.Decimal} (h₁ : some d₁ = Ext.Decimal.decimal s₁) : ExtFun.decimal.WellTyped [Validation.TypedExpr.lit (Prim.string s₁) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.decimal)
• lessThan {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtFun.lessThan.WellTyped [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• lessThanOrEqual {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtFun.lessThanOrEqual.WellTyped [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• greaterThan {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtFun.greaterThan.WellTyped [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• greaterThanOrEqual {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.decimal) : ExtFun.greaterThanOrEqual.WellTyped [x₁, x₂] (Validation.CedarType.bool Validation.BoolType.anyBool)
• ip {s₁ : String} {ip₁ : IPAddr} (h₁ : some ip₁ = Ext.IPAddr.ip s₁) : ExtFun.ip.WellTyped [Validation.TypedExpr.lit (Prim.string s₁) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.ipAddr)
• isIpv4 {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtFun.isIpv4.WellTyped [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isIpv6 {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtFun.isIpv6.WellTyped [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isLoopback {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtFun.isLoopback.WellTyped [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isMulticast {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtFun.isMulticast.WellTyped [x₁] (Validation.CedarType.bool Validation.BoolType.anyBool)
• isInRange {x₁ : Validation.TypedExpr} {xs : List Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) (h₂ : xs.length > 0) (h₃ : ∀ (x : Validation.TypedExpr), x ∈ xs → x.typeOf = Validation.CedarType.ext Validation.ExtType.ipAddr) : ExtFun.isInRange.WellTyped (x₁ :: xs) (Validation.CedarType.bool Validation.BoolType.anyBool)
• datetime {s₁ : String} {d₁ : Ext.Datetime} (h₁ : some d₁ = Ext.Datetime.parse s₁) : ExtFun.datetime.WellTyped [Validation.TypedExpr.lit (Prim.string s₁) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.datetime)
• duration {s₁ : String} {d₁ : Duration} (h₁ : some d₁ = Ext.Datetime.Duration.parse s₁) : ExtFun.duration.WellTyped [Validation.TypedExpr.lit (Prim.string s₁) Validation.CedarType.string] (Validation.CedarType.ext Validation.ExtType.duration)
• offset {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.offset.WellTyped [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.datetime)
• durationSince {x₁ x₂ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) (h₂ : x₂.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtFun.durationSince.WellTyped [x₁, x₂] (Validation.CedarType.ext Validation.ExtType.duration)
• toDate {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtFun.toDate.WellTyped [x₁] (Validation.CedarType.ext Validation.ExtType.datetime)
• toTime {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.datetime) : ExtFun.toTime.WellTyped [x₁] (Validation.CedarType.ext Validation.ExtType.duration)
• toMilliseconds {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.toMilliseconds.WellTyped [x₁] Validation.CedarType.int
• toSeconds {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.toSeconds.WellTyped [x₁] Validation.CedarType.int
• toMinutes {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.toMinutes.WellTyped [x₁] Validation.CedarType.int
• toHours {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.toHours.WellTyped [x₁] Validation.CedarType.int
• toDays {x₁ : Validation.TypedExpr} (h₁ : x₁.typeOf = Validation.CedarType.ext Validation.ExtType.duration) : ExtFun.toDays.WellTyped [x₁] Validation.CedarType.int

inductive Cedar.Thm.ExtHasAttrChainValid (ets : Validation.EntitySchema) : Validation.CedarType → List Spec.Attr → Prop

Chain validity for extended has attribute checks. Starting from a Cedar type, each intermediate attribute access in the chain must either:

• yield an entity or record type (so that attrsOf succeeds on the next value),
• not be present in the schema (absent attribute is valid). The LAST attribute in the chain doesn't need this constraint (we just check existence). In other words, a valid chain doesn't have intermediate accesses to attributes that are neither entitiy nor records.

• last {ets : Validation.EntitySchema} {ty : Validation.CedarType} {attr : Spec.Attr} : ExtHasAttrChainValid ets ty [attr]

  A single-attribute chain is always valid (just a has check, no deeper traversal)

• cons_entity {ets : Validation.EntitySchema} {ety nextEty : Spec.EntityType} {attr : Spec.Attr} {rest : List Spec.Attr} {rty : Validation.RecordType} {qty : Validation.QualifiedType} (h₁ : ets.attrs? ety = some rty) (h₂ : Data.Map.find? rty attr = some qty) (h₃ : Validation.Qualified.getType qty = Validation.CedarType.entity nextEty) (h₄ : ExtHasAttrChainValid ets (Validation.CedarType.entity nextEty) rest) : ExtHasAttrChainValid ets (Validation.CedarType.entity ety) (attr :: rest)

  Intermediate attribute has entity type in the schema

• cons_record_from_entity {ets : Validation.EntitySchema} {ety : Spec.EntityType} {attr : Spec.Attr} {rest : List Spec.Attr} {rty : Validation.RecordType} {qty : Validation.QualifiedType} {recRty : Validation.RecordType} (h₁ : ets.attrs? ety = some rty) (h₂ : Data.Map.find? rty attr = some qty) (h₃ : Validation.Qualified.getType qty = Validation.CedarType.record recRty) (h₄ : ExtHasAttrChainValid ets (Validation.CedarType.record recRty) rest) : ExtHasAttrChainValid ets (Validation.CedarType.entity ety) (attr :: rest)

  Intermediate attribute has record type in the schema

• cons_not_in_schema_entity {ets : Validation.EntitySchema} {ety : Spec.EntityType} {attr : Spec.Attr} {rest : List Spec.Attr} (h₁ : ets.attrs? ety = none ∨ ∀ (rty : Validation.RecordType), ets.attrs? ety = some rty → Data.Map.find? rty attr = none) : ExtHasAttrChainValid ets (Validation.CedarType.entity ety) (attr :: rest)

  Attribute not found in schema for entity — chain is vacuously valid (at runtime, find? will return .none → .ok false)

• cons_entity_from_record {ets : Validation.EntitySchema} {recRty : Validation.RecordType} {attr : Spec.Attr} {rest : List Spec.Attr} {qty : Validation.QualifiedType} {nextEty : Spec.EntityType} (h₁ : Data.Map.find? recRty attr = some qty) (h₂ : Validation.Qualified.getType qty = Validation.CedarType.entity nextEty) (h₃ : ExtHasAttrChainValid ets (Validation.CedarType.entity nextEty) rest) : ExtHasAttrChainValid ets (Validation.CedarType.record recRty) (attr :: rest)

  Record type: intermediate attribute has entity type

• cons_record_from_record {ets : Validation.EntitySchema} {recRty : Validation.RecordType} {attr : Spec.Attr} {rest : List Spec.Attr} {qty : Validation.QualifiedType} {nextRecRty : Validation.RecordType} (h₁ : Data.Map.find? recRty attr = some qty) (h₂ : Validation.Qualified.getType qty = Validation.CedarType.record nextRecRty) (h₃ : ExtHasAttrChainValid ets (Validation.CedarType.record nextRecRty) rest) : ExtHasAttrChainValid ets (Validation.CedarType.record recRty) (attr :: rest)

  Record type: intermediate attribute has record type

• cons_not_in_record {ets : Validation.EntitySchema} {recRty : Validation.RecordType} {attr : Spec.Attr} {rest : List Spec.Attr} (h₁ : Data.Map.find? recRty attr = none) : ExtHasAttrChainValid ets (Validation.CedarType.record recRty) (attr :: rest)

  Record type: attribute not in record type — vacuously valid

inductive Cedar.Thm.TypedExpr.WellTyped (env : Validation.TypeEnv) : Validation.TypedExpr → Prop

• lit {env : Validation.TypeEnv} {p : Spec.Prim} {ty : Validation.CedarType} (h₁ : Spec.Prim.WellTyped env p ty) : WellTyped env (Validation.TypedExpr.lit p ty)
• var {env : Validation.TypeEnv} {v : Spec.Var} {ty : Validation.CedarType} (h₁ : Spec.Var.WellTyped env v ty) : WellTyped env (Validation.TypedExpr.var v ty)
• ite {env : Validation.TypeEnv} {x₁ x₂ x₃ : Validation.TypedExpr} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : WellTyped env x₃) (h₄ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₅ : x₂.typeOf = x₃.typeOf) : WellTyped env (x₁.ite x₂ x₃ x₂.typeOf)
• and {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.and x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
• or {env : Validation.TypeEnv} {x₁ x₂ : Validation.TypedExpr} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : x₁.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) (h₄ : x₂.typeOf = Validation.CedarType.bool Validation.BoolType.anyBool) : WellTyped env (x₁.or x₂ (Validation.CedarType.bool Validation.BoolType.anyBool))
• unaryApp {env : Validation.TypeEnv} {op₁ : Spec.UnaryOp} {x₁ : Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : op₁.WellTyped x₁ ty) : WellTyped env (Validation.TypedExpr.unaryApp op₁ x₁ ty)
• binaryApp {env : Validation.TypeEnv} {op₂ : Spec.BinaryOp} {x₁ x₂ : Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : WellTyped env x₂) (h₃ : Spec.BinaryOp.WellTyped env op₂ x₁ x₂ ty) : WellTyped env (Validation.TypedExpr.binaryApp op₂ x₁ x₂ ty)
• hasAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
• hasAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) : WellTyped env (x₁.hasAttr attr (Validation.CedarType.bool Validation.BoolType.anyBool))
• extHasAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} {attrs : List Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) (h₃ : ExtHasAttrChainValid env.ets (Validation.CedarType.entity ety) (attr :: attrs)) : WellTyped env (x₁.extHasAttr attr attrs (Validation.CedarType.bool Validation.BoolType.anyBool))
• extHasAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} {attrs : List Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) (h₃ : ExtHasAttrChainValid env.ets (Validation.CedarType.record rty) (attr :: attrs)) : WellTyped env (x₁.extHasAttr attr attrs (Validation.CedarType.bool Validation.BoolType.anyBool))
• extHasAttr_ff {env : Validation.TypeEnv} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} {attrs : List Spec.Attr} (h₁ : WellTyped env x₁) (h₂ : (∃ (ety : Spec.EntityType), x₁.typeOf = Validation.CedarType.entity ety) ∨ ∃ (rty : Data.Map Spec.Attr (Validation.Qualified Validation.CedarType)), x₁.typeOf = Validation.CedarType.record rty) (h₃ : ExtHasAttrChainValid env.ets x₁.typeOf (attr :: attrs)) : WellTyped env (x₁.extHasAttr attr attrs (Validation.CedarType.bool Validation.BoolType.anyBool))
• getAttr_entity {env : Validation.TypeEnv} {ety : Spec.EntityType} {rty : Validation.RecordType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.entity ety) (h₃ : Option.map Validation.RecordType.liftBoolTypes (env.ets.attrs? ety) = some rty) (h₄ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
• getAttr_record {env : Validation.TypeEnv} {rty : Validation.RecordType} {x₁ : Validation.TypedExpr} {attr : Spec.Attr} {ty : Validation.CedarType} (h₁ : WellTyped env x₁) (h₂ : x₁.typeOf = Validation.CedarType.record rty) (h₃ : Option.map Validation.Qualified.getType (Data.Map.find? rty attr) = some ty) : WellTyped env (x₁.getAttr attr ty)
• set {env : Validation.TypeEnv} {ls : List Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : ∀ (x : Validation.TypedExpr), x ∈ ls → WellTyped env x) (h₂ : ∀ (x : Validation.TypedExpr), x ∈ ls → x.typeOf = ty) (h₃ : (ls != []) = true) : WellTyped env (Validation.TypedExpr.set ls ty.set)
• record {env : Validation.TypeEnv} {rty : Validation.RecordType} {m : List (Spec.Attr × Validation.TypedExpr)} (h₁ : ∀ (k : Spec.Attr) (v : Validation.TypedExpr), (k, v) ∈ m → WellTyped env v) (h₂ : rty = Data.Map.make (List.map (fun (x : Spec.Attr × Validation.TypedExpr) => match x with | (a, ty) => (a, Validation.Qualified.required ty.typeOf)) m)) : WellTyped env (Validation.TypedExpr.record m (Validation.CedarType.record rty))
• call {env : Validation.TypeEnv} {xfn : Spec.ExtFun} {args : List Validation.TypedExpr} {ty : Validation.CedarType} (h₁ : ∀ (x : Validation.TypedExpr), x ∈ args → WellTyped env x) (h₂ : xfn.WellTyped args ty) : WellTyped env (Validation.TypedExpr.call xfn args ty)