summaryrefslogtreecommitdiff
path: root/tests/hol4/misc-constants
diff options
context:
space:
mode:
authorSon Ho2023-09-07 16:06:14 +0200
committerSon Ho2023-09-07 16:06:14 +0200
commitce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch)
tree933d2bd806026930d216e4f16f113ea2749ca250 /tests/hol4/misc-constants
parent1181aecddbcb3232c21b191fbde59c2e9596846a (diff)
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/hol4/misc-constants')
-rw-r--r--tests/hol4/misc-constants/constantsScript.sml10
-rw-r--r--tests/hol4/misc-constants/constantsTheory.sig12
2 files changed, 2 insertions, 20 deletions
diff --git a/tests/hol4/misc-constants/constantsScript.sml b/tests/hol4/misc-constants/constantsScript.sml
index d589d348..40a319c6 100644
--- a/tests/hol4/misc-constants/constantsScript.sml
+++ b/tests/hol4/misc-constants/constantsScript.sml
@@ -13,17 +13,9 @@ Definition x0_c_def:
x0_c : u32 = get_return_value x0_body
End
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
- core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
- core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
(** [constants::X1] *)
Definition x1_body_def:
- x1_body : u32 result = Return core_num_u32_max_c
+ x1_body : u32 result = Return core_u32_max
End
Definition x1_c_def:
x1_c : u32 = get_return_value x1_body
diff --git a/tests/hol4/misc-constants/constantsTheory.sig b/tests/hol4/misc-constants/constantsTheory.sig
index 149d7e22..287ad5f5 100644
--- a/tests/hol4/misc-constants/constantsTheory.sig
+++ b/tests/hol4/misc-constants/constantsTheory.sig
@@ -4,8 +4,6 @@ sig
(* Definitions *)
val add_fwd_def : thm
- val core_num_u32_max_body_def : thm
- val core_num_u32_max_c_def : thm
val get_z1_fwd_def : thm
val get_z1_z1_body_def : thm
val get_z1_z1_c_def : thm
@@ -110,14 +108,6 @@ sig
⊢ ∀a b. add_fwd a b = i32_add a b
- [core_num_u32_max_body_def] Definition
-
- ⊢ core_num_u32_max_body = Return (int_to_u32 4294967295)
-
- [core_num_u32_max_c_def] Definition
-
- ⊢ core_num_u32_max_c = get_return_value core_num_u32_max_body
-
[get_z1_fwd_def] Definition
⊢ get_z1_fwd = Return get_z1_z1_c
@@ -321,7 +311,7 @@ sig
[x1_body_def] Definition
- ⊢ x1_body = Return core_num_u32_max_c
+ ⊢ x1_body = Return core_u32_max
[x1_c_def] Definition