diff options
| author | Son Ho | 2023-12-05 17:34:13 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-05 17:34:13 +0100 |
| commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
| tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/hol4/misc-constants | |
| parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
| parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) | |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'tests/hol4/misc-constants')
| -rw-r--r-- | tests/hol4/misc-constants/constantsScript.sml | 10 | ||||
| -rw-r--r-- | tests/hol4/misc-constants/constantsTheory.sig | 12 |
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 |