inductive Cedar.Validation.TypeError : Type

• lubErr (ty₁ ty₂ : CedarType) : TypeError
• unexpectedType (ty : CedarType) : TypeError
• attrNotFound (ty : CedarType) (attr : Spec.Attr) : TypeError
• tagNotFound (ety : Spec.EntityType) (tag : Spec.Expr) : TypeError
• unknownEntity (ety : Spec.EntityType) : TypeError
• extensionErr (xs : List Spec.Expr) : TypeError
• emptySetErr : TypeError
• incompatibleSetTypes (ty : List CedarType) : TypeError

instance Cedar.Validation.instReprTypeError : Repr TypeError

Equations

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

def Cedar.Validation.instReprTypeError.repr : TypeError → Nat → Std.Format

Equations

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

def Cedar.Validation.instDecidableEqTypeError.decEq (x✝ x✝¹ : TypeError) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.unexpectedType ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.attrNotFound ty attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.lubErr ty₁ ty₂) (Cedar.Validation.TypeError.incompatibleSetTypes ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType a) (Cedar.Validation.TypeError.unexpectedType b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.attrNotFound ty_1 attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unexpectedType ty) (Cedar.Validation.TypeError.incompatibleSetTypes ty_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.unexpectedType ty_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.attrNotFound ty attr) (Cedar.Validation.TypeError.incompatibleSetTypes ty_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.unexpectedType ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.attrNotFound ty attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.unknownEntity ety_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.tagNotFound ety tag) (Cedar.Validation.TypeError.incompatibleSetTypes ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.unexpectedType ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.attrNotFound ty attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.tagNotFound ety_1 tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity a) (Cedar.Validation.TypeError.unknownEntity b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.unknownEntity ety) (Cedar.Validation.TypeError.incompatibleSetTypes ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.unexpectedType ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.attrNotFound ty attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr a) (Cedar.Validation.TypeError.extensionErr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.extensionErr xs) (Cedar.Validation.TypeError.incompatibleSetTypes ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.unexpectedType ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.attrNotFound ty attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr Cedar.Validation.TypeError.emptySetErr = isTrue ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq Cedar.Validation.TypeError.emptySetErr (Cedar.Validation.TypeError.incompatibleSetTypes ty) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.lubErr ty₁ ty₂) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.unexpectedType ty_1) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.attrNotFound ty_1 attr) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.tagNotFound ety tag) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.unknownEntity ety) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) (Cedar.Validation.TypeError.extensionErr xs) = isFalse ⋯
• Cedar.Validation.instDecidableEqTypeError.decEq (Cedar.Validation.TypeError.incompatibleSetTypes ty) Cedar.Validation.TypeError.emptySetErr = isFalse ⋯

instance Cedar.Validation.instDecidableEqTypeError : DecidableEq TypeError

Equations

• Cedar.Validation.instDecidableEqTypeError = Cedar.Validation.instDecidableEqTypeError.decEq

inductive Cedar.Validation.Key : Type

• attr (a : Spec.Attr) : Key
• tag (x : Spec.Expr) : Key

instance Cedar.Validation.instReprKey : Repr Key

Equations

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

def Cedar.Validation.instReprKey.repr : Key → Nat → Std.Format

Equations

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

instance Cedar.Validation.instDecidableEqKey : DecidableEq Key

Equations

• Cedar.Validation.instDecidableEqKey = Cedar.Validation.instDecidableEqKey.decEq

def Cedar.Validation.instDecidableEqKey.decEq (x✝ x✝¹ : Key) : Decidable (x✝ = x✝¹)

Equations

• Cedar.Validation.instDecidableEqKey.decEq (Cedar.Validation.Key.attr a) (Cedar.Validation.Key.attr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Cedar.Validation.instDecidableEqKey.decEq (Cedar.Validation.Key.attr a) (Cedar.Validation.Key.tag x_2) = isFalse ⋯
• Cedar.Validation.instDecidableEqKey.decEq (Cedar.Validation.Key.tag x_2) (Cedar.Validation.Key.attr a) = isFalse ⋯
• Cedar.Validation.instDecidableEqKey.decEq (Cedar.Validation.Key.tag a) (Cedar.Validation.Key.tag b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[reducible, inline]

abbrev Cedar.Validation.Capabilities : Type

Equations

• Cedar.Validation.Capabilities = List (Cedar.Spec.Expr × Cedar.Validation.Key)

def Cedar.Validation.Capabilities.singleton (e : Spec.Expr) (k : Key) : Capabilities

Equations

• Cedar.Validation.Capabilities.singleton e k = [(e, k)]

@[reducible, inline]

abbrev Cedar.Validation.ResultType : Type

Equations

• Cedar.Validation.ResultType = Except Cedar.Validation.TypeError (Cedar.Validation.TypedExpr × Cedar.Validation.Capabilities)

def Cedar.Validation.ResultType.typeOf : ResultType → Except TypeError (CedarType × Capabilities)

Equations

• Cedar.Validation.ResultType.typeOf = Except.map fun (x : Cedar.Validation.TypedExpr × Cedar.Validation.Capabilities) => match x with | (ty, c) => (ty.typeOf, c)

def Cedar.Validation.ok {α : Type} (ty : α) (c : Capabilities := ∅) : Except TypeError (α × Capabilities)

Equations

• Cedar.Validation.ok ty c = Except.ok (ty, c)

def Cedar.Validation.err {α : Type} (e : TypeError) : Except TypeError (α × Capabilities)

Equations

• Cedar.Validation.err e = Except.error e

def Cedar.Validation.typeOfLit (p : Spec.Prim) (env : TypeEnv) : ResultType

Equations

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

def Cedar.Validation.typeOfVar (v : Spec.Var) (env : TypeEnv) : ResultType

Equations

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

def Cedar.Validation.typeOfIf (r₁ : TypedExpr × Capabilities) (r₂ r₃ : ResultType) : ResultType

Equations

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

def Cedar.Validation.typeOfAnd (r₁ : TypedExpr × Capabilities) (r₂ : ResultType) : ResultType

Equations

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

def Cedar.Validation.typeOfOr (r₁ : TypedExpr × Capabilities) (r₂ : ResultType) : ResultType

Equations

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

def Cedar.Validation.typeOfUnaryApp (op : Spec.UnaryOp) (ty : TypedExpr) : ResultType

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOfUnaryApp op✝ ty = Cedar.Validation.err (Cedar.Validation.TypeError.unexpectedType ty.typeOf)

def Cedar.Validation.typeOfEq (ty₁ ty₂ : TypedExpr) (x₁ x₂ : Spec.Expr) : ResultType

Equations

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

def Cedar.Validation.entityUID? : Spec.Expr → Option Spec.EntityUID

Equations

• Cedar.Validation.entityUID? (Cedar.Spec.Expr.lit (Cedar.Spec.Prim.entityUID uid)) = some uid
• Cedar.Validation.entityUID? x✝ = none

def Cedar.Validation.entityUIDs? : Spec.Expr → Option (List Spec.EntityUID)

Equations

• Cedar.Validation.entityUIDs? (Cedar.Spec.Expr.set xs) = List.mapM Cedar.Validation.entityUID? xs
• Cedar.Validation.entityUIDs? x✝ = none

def Cedar.Validation.actionUID? (x : Spec.Expr) (acts : ActionSchema) : Option Spec.EntityUID

Equations

• Cedar.Validation.actionUID? x acts = do let uid ← Cedar.Validation.entityUID? x if acts.contains uid = true then some uid else none

def Cedar.Validation.typeOfInₑ (ety₁ ety₂ : Spec.EntityType) (x₁ x₂ : Spec.Expr) (env : TypeEnv) : BoolType

Equations

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

def Cedar.Validation.typeOfInₛ (ety₁ ety₂ : Spec.EntityType) (x₁ x₂ : Spec.Expr) (env : TypeEnv) : BoolType

Equations

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

def Cedar.Validation.typeOfHasTag (ety : Spec.EntityType) (x t : Spec.Expr) (c : Capabilities) (env : TypeEnv) : Except TypeError (CedarType × Capabilities)

Equations

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

def Cedar.Validation.typeOfGetTag (ety : Spec.EntityType) (x t : Spec.Expr) (c : Capabilities) (env : TypeEnv) : Except TypeError (CedarType × Capabilities)

Equations

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

def Cedar.Validation.ifLubThenBool (ty₁ ty₂ : CedarType) : Except TypeError (CedarType × Capabilities)

Equations

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

def Cedar.Validation.typeOfBinaryApp (op₂ : Spec.BinaryOp) (ty₁ ty₂ : TypedExpr) (x₁ x₂ : Spec.Expr) (c : Capabilities) (env : TypeEnv) : ResultType

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOfBinaryApp Cedar.Spec.BinaryOp.eq ty₁ ty₂ x₁ x₂ c env = Cedar.Validation.typeOfEq ty₁ ty₂ x₁ x₂
• Cedar.Validation.typeOfBinaryApp op₂✝ ty₁ ty₂ x₁ x₂ c env = Cedar.Validation.err (Cedar.Validation.TypeError.unexpectedType ty₁.typeOf)

def Cedar.Validation.hasAttrInRecord (rty : RecordType) (x : Spec.Expr) (a : Spec.Attr) (c : Capabilities) (knownToExist : Bool) : Except TypeError (CedarType × Capabilities)

Equations

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

def Cedar.Validation.typeOfHasAttr (ty : TypedExpr) (x : Spec.Expr) (a : Spec.Attr) (c : Capabilities) (env : TypeEnv) : ResultType

Equations

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

def Cedar.Validation.getAttrInRecord (ty : CedarType) (rty : RecordType) (x : Spec.Expr) (a : Spec.Attr) (c : Capabilities) : Except TypeError (CedarType × Capabilities)

Equations

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

def Cedar.Validation.typeOfGetAttr (ty : TypedExpr) (x : Spec.Expr) (a : Spec.Attr) (c : Capabilities) (env : TypeEnv) : ResultType

Equations

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

def Cedar.Validation.typeOfSet (tys : List TypedExpr) : ResultType

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOfSet [] = Cedar.Validation.err Cedar.Validation.TypeError.emptySetErr

@[inline]

def Cedar.Validation.justType (r : ResultType) : Except TypeError TypedExpr

Equations

• Cedar.Validation.justType r = Except.map Prod.fst r

def Cedar.Validation.typeOfConstructor {α : Type u_1} (mk : String → Option α) (xs : List Spec.Expr) (ty : CedarType) : Except TypeError (CedarType × Capabilities)

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOfConstructor mk xs ty = Cedar.Validation.err (Cedar.Validation.TypeError.extensionErr xs)

def Cedar.Validation.typeOfCall (xfn : Spec.ExtFun) (tys : List TypedExpr) (xs : List Spec.Expr) : ResultType

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOfCall xfn✝ tys xs = Cedar.Validation.err (Cedar.Validation.TypeError.extensionErr xs)

@[irreducible]

def Cedar.Validation.typeOf (x : Spec.Expr) (c : Capabilities) (env : TypeEnv) : ResultType

Equations

• One or more equations did not get rendered due to their size.
• Cedar.Validation.typeOf (Cedar.Spec.Expr.lit p) c env = Cedar.Validation.typeOfLit p env
• Cedar.Validation.typeOf (Cedar.Spec.Expr.var v) c env = Cedar.Validation.typeOfVar v env
• Cedar.Validation.typeOf (Cedar.Spec.Expr.unaryApp op₁ x₁) c env = do let __discr ← Cedar.Validation.typeOf x₁ c env match __discr with | (ty₁, snd) => Cedar.Validation.typeOfUnaryApp op₁ ty₁
• Cedar.Validation.typeOf (x₁.hasAttr a) c env = do let __discr ← Cedar.Validation.typeOf x₁ c env match __discr with | (ty₁, snd) => Cedar.Validation.typeOfHasAttr ty₁ x₁ a c env
• Cedar.Validation.typeOf (x₁.getAttr a) c env = do let __discr ← Cedar.Validation.typeOf x₁ c env match __discr with | (ty₁, snd) => Cedar.Validation.typeOfGetAttr ty₁ x₁ a c env

instance Cedar.Validation.instReprRequestType : Repr RequestType

Equations

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

def Cedar.Validation.instReprRequestType.repr : RequestType → Nat → Std.Format

Equations

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

def Cedar.Validation.instReprTypeEnv.repr : TypeEnv → Nat → Std.Format

Equations

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

instance Cedar.Validation.instReprTypeEnv : Repr TypeEnv

Equations

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