diff options
Diffstat (limited to 'backends/hol4/primitivesTheory.sig')
-rw-r--r-- | backends/hol4/primitivesTheory.sig | 6 |
1 files changed, 6 insertions, 0 deletions
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) |