theorem
Cedar.Thm.ext_well_typed_after_map
{xfn : Spec.ExtFun}
{args : List Spec.Residual}
{ty : Validation.CedarType}
{env : Validation.TypeEnv}
{f : Spec.Residual → Spec.Residual}
:
Spec.ExtResidualWellTyped xfn args ty →
(∀ (arg : Spec.Residual), arg ∈ args → Residual.WellTyped env arg → Residual.WellTyped env (f arg)) →
(∀ (arg : Spec.Residual), arg ∈ args → (f arg).typeOf = arg.typeOf) →
(∀ (x : Spec.Residual), x.asValue.isSome = true → f x = x) → Spec.ExtResidualWellTyped xfn (List.map f args) ty
theorem
Cedar.Thm.partial_eval_well_typed_call
{env : Validation.TypeEnv}
{xfn : Spec.ExtFun}
{args : List Spec.Residual}
{ty : Validation.CedarType}
{req : Spec.Request}
{preq : TPE.PartialRequest}
{es : Spec.Entities}
{pes : TPE.PartialEntities}
:
(∀ (r : Spec.Residual), r ∈ args → Residual.WellTyped env (TPE.evaluate env r preq pes)) →
PEWellTyped env (Spec.Residual.call xfn args ty) (TPE.evaluate env (Spec.Residual.call xfn args ty) preq pes) req preq
es pes