This file contains the theorems that TypedExpr.WellTyped implies CedarType.WellFormed.

@[irreducible]

theorem Cedar.Thm.well_typed_implies_wf_type {env : Validation.TypeEnv} {tx : Validation.TypedExpr} (hwf_env : env.WellFormed) (hwt : TypedExpr.WellTyped env tx) : Validation.CedarType.WellFormed env tx.typeOf

TypedExpr.WellTyped implies well-formedness of the type (CedarType.WellFormed).

theorem Cedar.Thm.typechecked_has_well_formed_type {e : Spec.Expr} {c₁ c₂ : Validation.Capabilities} {env : Validation.TypeEnv} {tx : Validation.TypedExpr} (hwf : env.WellFormed) (hty : Validation.typeOf e c₁ env = Except.ok (tx, c₂)) : Validation.CedarType.WellFormed env tx.typeOf

The result of typeOf has a well-formed type.