PureLang, ThunkLang, and EnvLang all use a function called apply_closure in their semantics. With the changes from #31, this seems unnecessary - apply_closure should instead be replaced by straightforward function application. This should simplify various proofs, particularly in ThunkLang where removing lemmas concerning apply_closure will likely streamline things.
Care needs to be taken for Ret/Raise in ThunkLang/EnvLang - these are now call-by-value, i.e. they evaluate the contained argument no matter what. This is achieved by a combination of with_value/apply_closure currently.
PureLang, ThunkLang, and EnvLang all use a function called
apply_closurein their semantics. With the changes from #31, this seems unnecessary -apply_closureshould instead be replaced by straightforward function application. This should simplify various proofs, particularly in ThunkLang where removing lemmas concerningapply_closurewill likely streamline things.Care needs to be taken for
Ret/Raisein ThunkLang/EnvLang - these are now call-by-value, i.e. they evaluate the contained argument no matter what. This is achieved by a combination ofwith_value/apply_closurecurrently.