lib: change runErrorT to runExceptT to match Haskell code

seL4 · Sep 4, 2018 · 0044c57 · 0044c57
1 parent 378717b
commit 0044c57
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy
@@ -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)"

diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy
@@ -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)

diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy
@@ -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)

diff --git a/proof/crefine/X64/Syscall_C.thy b/proof/crefine/X64/Syscall_C.thy
@@ -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)