From a8cf54cd23b8bd8c4cb5690ebee48a4086c4ca8d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 1 Feb 2023 00:40:13 +0100
Subject: Cleanup a bit and reorganize

---
 backends/hol4/primitivesTheory.sig | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'backends/hol4/primitivesTheory.sig')

diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index cf550f00..fdf28172 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -86,6 +86,7 @@ sig
     val i8_rem_def : thm
     val i8_sub_def : thm
     val int_rem_def : thm
+    val is_diverge_def : thm
     val isize_add_def : thm
     val isize_div_def : thm
     val isize_mul_def : thm
@@ -646,6 +647,11 @@ sig
           int_rem x y =
           if x ≥ 0 ∧ y ≥ 0 ∨ x < 0 ∧ y < 0 then x % y else -(x % y)
    
+   [is_diverge_def]  Definition
+      
+      ⊢ ∀r. is_diverge r ⇔
+            case r of Return v2 => F | Fail v3 => F | Diverge => T
+   
    [isize_add_def]  Definition
       
       ⊢ ∀x y. isize_add x y = mk_isize (isize_to_int x + isize_to_int y)
-- 
cgit v1.2.3