This file contains theorems about partial evaluation preserving well-typedness of residuals.

@[irreducible]

theorem Cedar.Thm.partial_eval_preserves_well_typed {env : Validation.TypeEnv} {res : Spec.Residual} {req : Spec.Request} {preq : TPE.PartialRequest} {es : Spec.Entities} {pes : TPE.PartialEntities} : InstanceOfWellFormedEnvironment req es env → RequestAndEntitiesRefine req es preq pes → Residual.WellTyped env res → Residual.WellTyped env (TPE.evaluate res preq pes)

Theorem: Partial evaluation preserves well-typedness of residuals.

If a residual is well-typed in some type environment, then partially evaluating it with a partial request and partial entities produces another well-typed residual in the same type environment.

This is a fundamental property ensuring that the partial evaluation process maintains type safety throughout the computation.