This file contains well-typedness theorems of TypedExpr

theorem Cedar.Thm.well_typed_is_sound {ty : Validation.TypedExpr} {v : Spec.Value} {env : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} : InstanceOfWellFormedEnvironment request entities env → TypedExpr.WellTyped env ty → Spec.evaluate ty.toExpr request entities = Except.ok v → InstanceOfType env v ty.typeOf

Successful evaluation of a well-typed expression should produce a value of corresponding type.