adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

lib: remove opt_mapE from global [elim!] set 

While we do want to break up full OptionMonad terms in assumptions, we
do not usually want to break up projections.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein 2023-02-01 18:21:08 +11:00 committed by Gerwin Klein
parent 3c322eab1d
commit 3467e685b6
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/Monads/OptionMonad.thy
View File

@ -416,7 +416,7 @@ lemma oreturnOkE:
by simp
lemmas omonadE [elim!] =
opt_mapE obindE oreturnE ofailE othrowE oreturnOkE oassertE
obindE oreturnE ofailE othrowE oreturnOkE oassertE
lemma in_opt_map_Some_eq:
"((f ||> g) x = Some y) = (\<exists>v. f x = Some v \<and> g v = y)"