diff options
| author | Son Ho | 2022-02-07 10:38:32 +0100 |
|---|---|---|
| committer | Son Ho | 2022-02-07 10:38:32 +0100 |
| commit | 4f116135d0c5abe98aaa763664c7ac33a7084c36 (patch) | |
| tree | a2fd0d700d9f4c389c09480f4655080c382c57e8 /fstar | |
| parent | 63dbf03303afa9c433595a25d0bab78d9d29561b (diff) | |
Make minor modifications to Primitives.fst
Diffstat (limited to 'fstar')
| -rw-r--r-- | fstar/Primitives.fst | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/fstar/Primitives.fst b/fstar/Primitives.fst index 46fa2d87..dae73f46 100644 --- a/fstar/Primitives.fst +++ b/fstar/Primitives.fst @@ -24,6 +24,7 @@ type char = FStar.Char.char (*** Scalars *) /// Rk.: most of the following code was at least partially generated + let isize_min : int = -9223372036854775808 let isize_max : int = 9223372036854775807 let i8_min : int = -128 @@ -37,7 +38,7 @@ let i64_max : int = 9223372036854775807 let i128_min : int = -170141183460469231731687303715884105728 let i128_max : int = 170141183460469231731687303715884105727 let usize_min : int = 0 -let usize_max : int = 18446744073709551615 +let usize_max : int = 4294967295 // being conservative here: [u32_max] instead of [u64_max] let u8_min : int = 0 let u8_max : int = 255 let u16_min : int = 0 |