diff options
Diffstat (limited to 'src/lem_interp/interp_lib.lem')
| -rw-r--r-- | src/lem_interp/interp_lib.lem | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/lem_interp/interp_lib.lem b/src/lem_interp/interp_lib.lem index c5c550da..3cbef5c8 100644 --- a/src/lem_interp/interp_lib.lem +++ b/src/lem_interp/interp_lib.lem @@ -26,16 +26,16 @@ let hardware_quot (a:integer) (b:integer) : integer = else a/b -let (max_64u : integer) = Num_extra.integerOfString "18446744073709551615" -let (max_64 : integer) = Num_extra.integerOfString "9223372036854775807" -let (min_64 : integer) = Num_extra.integerOfString "-9223372036854775808" -let (max_32u : integer) = Num_extra.integerOfString "4294967295" -let (max_32 : integer) = Num_extra.integerOfString "2147483647" -let (min_32 : integer) = Num_extra.integerOfString "-2147483648" -let (max_8 : integer) = (integerFromNat 127) -let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128) -let (max_5 : integer) = (integerFromNat 31) -let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32) +let (max_64u : integer) = integerFromNat ((natPow 2 64) - 1) +let (max_64 : integer) = integerFromNat ((natPow 2 63) - 1) +let (min_64 : integer) = integerNegate (integerFromNat (natPow 2 63)) +let (max_32u : integer) = integerFromNat 4294967295 +let (max_32 : integer) = integerFromNat 2147483647 +let (min_32 : integer) = integerNegate (integerFromNat 2147483648) +let (max_8 : integer) = (integerFromNat 127) +let (min_8 : integer) = (integerFromNat 0) - (integerFromNat 128) +let (max_5 : integer) = (integerFromNat 31) +let (min_5 : integer) = (integerFromNat 0)-(integerFromNat 32) val get_max_representable_in : signed -> nat -> integer let get_max_representable_in sign n = |