Typechecked is well typed after lifting
Cedar.Thm.typechecked_is_well_typed_after_lifting
Plain-language statement
The type checker produces typed expressions that are well-typed after type lifting. TODO: move this around after the proof is fixed
Exact Lean statement
theorem typechecked_is_well_typed_after_lifting
{e : Expr}
{c₁ c₂ : Capabilities}
{env : TypeEnv}
{ty : TypedExpr} :
typeOf e c₁ env = .ok (ty, c₂) →
TypedExpr.WellTyped env ty.liftBoolTypesFormal artifact
Lean source
theorem typechecked_is_well_typed_after_lifting{e : Expr}{c₁ c₂ : Capabilities}{env : TypeEnv}{ty : TypedExpr} : typeOf e c₁ env = .ok (ty, c₂) → TypedExpr.WellTyped env ty.liftBoolTypes:= by induction e, c₁ using typeOf.induct generalizing ty c₂ case _ => exact typechecked_is_well_typed_after_lifting_lit case _ => exact typechecked_is_well_typed_after_lifting_var case _ hᵢ₁ hᵢ₂ hᵢ₃ => exact typechecked_is_well_typed_after_lifting_ite hᵢ₁ hᵢ₂ hᵢ₃ case _ hᵢ₁ hᵢ₂ => exact typechecked_is_well_typed_after_lifting_and hᵢ₁ hᵢ₂ case _ hᵢ₁ hᵢ₂ => exact typechecked_is_well_typed_after_lifting_or hᵢ₁ hᵢ₂ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_unary_app hᵢ case _ hᵢ₁ hᵢ₂ => exact typechecked_is_well_typed_after_lifting_binary_app hᵢ₁ hᵢ₂ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_has_attr hᵢ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_get_attr hᵢ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_set hᵢ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_record hᵢ case _ hᵢ => exact typechecked_is_well_typed_after_lifting_call hᵢ- Project
- Cedar Specification
- License
- Apache-2.0
- Commit
- 3f093947b8ae
- Source
- cedar-lean/Cedar/Thm/WellTyped/Expr/Typechecking.lean:1356-1388
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.