This file contains well-typedness theorems of Residual

theorem Cedar.Thm.residual_well_typed_is_sound {r : Spec.Residual} {v : Spec.Value} {env : Validation.TypeEnv} {request : Spec.Request} {entities : Spec.Entities} : InstanceOfWellFormedEnvironment request entities env → Residual.WellTyped env r → r.evaluate request entities = Except.ok v → InstanceOfType env v r.typeOf

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