monads/reader_option: add no_ofail_ask

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Jul 11, 2024 · 9646d32 · 9646d32
1 parent 94fdcd6
commit 9646d32
Showing 1 changed file with 4 additions and 0 deletions.
diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy
@@ -250,6 +250,10 @@ lemma no_ofail_ofail[wp]:
   "no_ofail \<bottom> ofail"
   by (simp add: no_ofail_def)
 
+lemma no_ofail_ask[wp]:
+  "no_ofail \<top> ask"
+  by (simp add: no_ofail_def)
+
 lemma no_ofail_asks_simp[simp]:
   "no_ofail P (asks f)"
   unfolding asks_def oreturn_def obind_def no_ofail_def