lib/monads: rename assert_opt_ovalid to oassert_opt_ovalid and make [wp]

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Mar 19, 2024 · 4db52e9 · 4db52e9
1 parent 688e55b
commit 4db52e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -129,7 +129,7 @@ lemma owhile_ovalid[wp]:
    apply auto
   done
 
-lemma assert_opt_ovalid:
+lemma oassert_opt_ovalid[wp]:
   "\<lblot>\<lambda>s. \<forall>y. x = Some y \<longrightarrow> Q y s\<rblot> oassert_opt x \<lblot>Q\<rblot>"
   unfolding oassert_opt_def
   by (case_tac x; wpsimp)