theorem
Cedar.Thm.partial_evaluate_is_sound_val
{v : Spec.Value}
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{ty : Validation.CedarType}
:
Except.toOption ((Spec.Residual.val v ty).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.val v ty) preq pes).evaluate req es)
theorem
Cedar.Thm.partial_evaluate_is_sound_var
{req : Spec.Request}
{es : Spec.Entities}
{preq : TPE.PartialRequest}
{pes : TPE.PartialEntities}
{v : Spec.Var}
{ty : Validation.CedarType}
(hâ‚„ : RequestAndEntitiesRefine req es preq pes)
:
Except.toOption ((Spec.Residual.var v ty).evaluate req es) = Except.toOption ((TPE.evaluate (Spec.Residual.var v ty) preq pes).evaluate req es)