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

lib: change runErrorT to runExceptT to match Haskell code

This commit is contained in:
Ilya Yanok 2018-08-26 19:56:30 +02:00 committed by Gerwin Klein
parent 378717bee0
commit 0044c57e14
4 changed files with 5 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/HaskellLib_H.thy
View File

@ -177,14 +177,14 @@ definition
"catMaybes \<equiv> (map the) \<circ> (filter isJust)"
definition
"runErrorT \<equiv> id"
"runExceptT \<equiv> id"
declare Just_def[simp] Nothing_def[simp] fromJust_def[simp]
isJust_def[simp] tail_def[simp] head_def[simp]
error_def[simp] reverse_def[simp] isNothing_def[simp]
maybeApply_def[simp] maybe_def[simp]
foldR_def[simp] elem_def[simp] notElem_def[simp]
catMaybes_def[simp] runErrorT_def[simp]
catMaybes_def[simp] runExceptT_def[simp]
definition
"headM L \<equiv> (case L of (h # t) \<Rightarrow> return h | _ \<Rightarrow> fail)"

2
proof/crefine/ARM/Syscall_C.thy
View File

@ -480,7 +480,7 @@ lemma handleInvocation_def2:
| Inl (Inr preempt) \<Rightarrow> throwError preempt
od
od"
apply (simp add: handleInvocation_def Syscall_H.syscall_def runErrorT_def
apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def
liftE_bindE cong: sum.case_cong)
apply (rule ext, (rule bind_apply_cong [OF refl])+)
apply (clarsimp simp: bind_assoc split: sum.split)

2
proof/crefine/ARM_HYP/Syscall_C.thy
View File

@ -480,7 +480,7 @@ lemma handleInvocation_def2:
| Inl (Inr preempt) \<Rightarrow> throwError preempt
od
od"
apply (simp add: handleInvocation_def Syscall_H.syscall_def runErrorT_def
apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def
liftE_bindE cong: sum.case_cong)
apply (rule ext, (rule bind_apply_cong [OF refl])+)
apply (clarsimp simp: bind_assoc split: sum.split)

2
proof/crefine/X64/Syscall_C.thy
View File

@ -468,7 +468,7 @@ lemma handleInvocation_def2:
| Inl (Inr preempt) \<Rightarrow> throwError preempt
od
od"
apply (simp add: handleInvocation_def Syscall_H.syscall_def runErrorT_def
apply (simp add: handleInvocation_def Syscall_H.syscall_def runExceptT_def
liftE_bindE cong: sum.case_cong)
apply (rule ext, (rule bind_apply_cong [OF refl])+)
apply (clarsimp simp: bind_assoc split: sum.split)