Documentation

Cedar.Thm.TPE.PreservesTypeOf

source
@[reducible, inline]
abbrev Cedar.Thm.PEPreservesTypeOf (res : Spec.Residual) :
Prop
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Cedar.Thm.partial_eval_preserves_typeof (res : Spec.Residual) :
    PEPreservesTypeOf res

    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.