diff options
| author | Son Ho | 2023-02-01 00:40:13 +0100 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:54:38 +0200 |
| commit | a8cf54cd23b8bd8c4cb5690ebee48a4086c4ca8d (patch) | |
| tree | 04a3de511a760beab50aca80538c469414464e37 /backends/hol4/primitivesTheory.sig | |
| parent | 26309503ab0d7710f03333d7762e484be94767e0 (diff) | |
Cleanup a bit and reorganize
Diffstat (limited to '')
| -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) |