Mostly Revert "change AsVal to be easier to use (like IntoVal)"
This mostly reverts commit 68965acf, except for the part that improves IntoVal.
While attempting to fix LambdaRust, I feel like the AsVal
change was a bad idea. is_Some
is used in plenty of places around Iris, and with AsVal
no longer using is_Some
, many things became harder to do. For example, I am currently stuck at the following goal
__view_subject__ : Forall AsVal el
============================
Forall (λ ei : expr, is_Some (to_val ei)) el
Given that there are just two proofs that benefit from the changed AsVal
, this does not seem worth it.