summaryrefslogtreecommitdiff
path: root/tests/lean/Constants.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/Constants.lean')
-rw-r--r--tests/lean/Constants.lean6
1 files changed, 1 insertions, 5 deletions
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 51b415d6..b0cdaa90 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -9,12 +9,8 @@ namespace constants
def x0_body : Result U32 := Result.ret (U32.ofInt 0)
def x0_c : U32 := eval_global x0_body (by simp)
-/- [core::num::u32::{8}::MAX] -/
-def core_num_u32_max_body : Result U32 := Result.ret (U32.ofInt 4294967295)
-def core_num_u32_max_c : U32 := eval_global core_num_u32_max_body (by simp)
-
/- [constants::X1] -/
-def x1_body : Result U32 := Result.ret core_num_u32_max_c
+def x1_body : Result U32 := Result.ret core_u32_max
def x1_c : U32 := eval_global x1_body (by simp)
/- [constants::X2] -/