Skip to content

Mostly Revert "change AsVal to be easier to use (like IntoVal)"

Ralf Jung requested to merge ralf/into_val into gen_proofmode

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.

Cc @jjourdan @robbertkrebbers

Merge request reports