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

lib: add some basic option monad functions 

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2021-02-11 08:45:16 +11:00 committed by Gerwin Klein
parent 65b7139398
commit f6d919f159
1 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/Monad_WP/OptionMonad.thy
View File

@ -100,6 +100,12 @@ definition oapply :: "'a \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow
definition oliftM :: "('a \<Rightarrow> 'b) \<Rightarrow> ('s,'a) lookup \<Rightarrow> ('s,'b) lookup" where
"oliftM f m \<equiv> do { x \<leftarrow> m; oreturn (f x) }"
definition ounless :: "bool \<Rightarrow> ('s, unit) lookup \<Rightarrow> ('s, unit) lookup" where
"ounless P f \<equiv> if P then oreturn () else f"
definition owhen :: "bool \<Rightarrow> ('s, unit) lookup \<Rightarrow> ('s, unit) lookup" where
"owhen P f \<equiv> if P then f else oreturn ()"
(* Reader monad interface: *)
abbreviation (input)
"ask \<equiv> Some"