Partial eval preserves typeof
Cedar.Thm.partial_eval_preserves_typeof
Plain-language statement
Theorem: TPE.evaluate preserves the typeOf property. If a residual has a certain type, then partially evaluating it produces a residual with the same type.
Exact Lean statement
theorem partial_eval_preserves_typeof : ∀ res, PEPreservesTypeOf res
Formal artifact
Lean source
theorem partial_eval_preserves_typeof : ∀ res, PEPreservesTypeOf res:= by intro res env cases res with | val v ty => simp [TPE.evaluate, Residual.typeOf] | var v ty => intro _ preq simp only [Residual.typeOf, TPE.evaluate] unfold varₚ simp only [varₚ.varₒ, someOrSelf] cases v with | principal => cases h: preq.principal.asEntityUID <;> simp | resource | action => cases h: preq.resource.asEntityUID <;> simp | context => cases h: preq.context <;> simp | error ty => simp [TPE.evaluate, Residual.typeOf] | and a b ty => exact partial_eval_preserves_typeof_and (partial_eval_preserves_typeof a) (partial_eval_preserves_typeof b) | or a b ty => exact partial_eval_preserves_typeof_or (partial_eval_preserves_typeof a) (partial_eval_preserves_typeof b) | ite c t e ty => exact partial_eval_preserves_typeof_ite (partial_eval_preserves_typeof t) (partial_eval_preserves_typeof e) | unaryApp op e ty => exact partial_eval_preserves_typeof_unaryApp | binaryApp op e1 e2 ty => exact partial_eval_preserves_typeof_binaryApp | call xfn args ty => exact partial_eval_preserves_typeof_call | getAttr expr attr ty => exact partial_eval_preserves_typeof_getAttr | hasAttr expr attr ty => exact partial_eval_preserves_typeof_hasAttr | set ls ty => exact partial_eval_preserves_typeof_set | record ls ty => exact partial_eval_preserves_typeof_record- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/TPE/PreservesTypeOf.lean:254-297
Reuse this declaration
Bring the exact result into your workflow
The import identifies the source module. Your project still needs the pinned package dependency shown on this page.
What this badge means
This completion status comes from the project or community source. It has not yet been represented here as an independent rebuild and axiom audit.
Continue in this project
Related declarations
Find? ext
Cedar.Data.Map.find?_ext
Plain-language statement
Two well-formed maps are equal if they have the same find? for every key.
Source project: Cedar Specification
Person-level attribution pending.
Find? notmem keys
Cedar.Data.Map.find?_notmem_keys
Plain-language statement
Inverse of find?_mem_toList, except that this requires wf
Source project: Cedar Specification
Person-level attribution pending.
Find? some iff in values
Cedar.Data.Map.find?_some_iff_in_values
Plain-language statement
The mp direction of this does not need the wf precondition and, in fact, is available separately as find?_some_implies_in_values above
Source project: Cedar Specification
Person-level attribution pending.