You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
A start of a proof of this once existed in cast-inert.agda but it's a little naïve. You need some sort of equality that lets you reason under binders because cast removal goes under binders -- or else you need to not really remove all the casts, which defeats the purpose. Removed this proof fragment before popl aoe because the static version that remains, just that the type doesn't change, is enough to back up the vague intuition we give in the paper. Developing an equational theory here would be an interesting future exercise.
A start of a proof of this once existed in
cast-inert.agda
but it's a little naïve. You need some sort of equality that lets you reason under binders because cast removal goes under binders -- or else you need to not really remove all the casts, which defeats the purpose. Removed this proof fragment before popl aoe because the static version that remains, just that the type doesn't change, is enough to back up the vague intuition we give in the paper. Developing an equational theory here would be an interesting future exercise.The text was updated successfully, but these errors were encountered: